Princess extensions: formal coverage
Parked overview · Companion proofs · Rectangle Lean coverage
Parked, with existing verification preserved. The complete physical and classifications remain Lean theorems. This reorganization neither adds nor withdraws a formal result.
Companion Lean package · Exact source scope · Existing compiler receipt
The three-cube theorem covers every positive daily budget, physical target walks, lower bounds and attaining inspections. The four-cube theorem covers every budget, including forty days at eight inspections and the shape-sensitive reduction needed to prove that minimum. The formal proofs allow arbitrary competing inspection sequences.
Generic strategy compression, finite subset certificates, physical belief semantics and related shared modules support these theorems. Each dependency remains in the canonical source directory and is included where needed in the downloadable package. The module manifest distinguishes shared tools from independent applications. No second authoritative version is maintained.
The general odd-box nesting theorem, the general side-of-length-two application, the classification, the families and the broader cylinder laws have ordinary mathematical proofs or finite certificates at their stated boundaries. They are not all completely formalized by the cube results or by the aggregate compiler receipt.
The existing source-specific check passed 83 modules in the combined development. This release checks that the distributed sources still match those hashes and that imports are closed. To reproduce a fresh compiler check, extract this package and run python3 src/check_lean.py --lean /path/to/lean with Lean 4.33.1. Read the included guide for its exact scope.
The unresolved formalization of independent companion geometry is parked. It is not a condition for completing the main rectangle paper.
The companion package contains 51 modules, including eleven dependencies shared with the 43-module rectangle package. There are 83 canonical modules in total; distribution copies are not separate authoritative proofs.