num_octants
plain-language theorem explainer
The definition assigns the integer 8 to the number of octants in three-dimensional space. Researchers deriving the recognition wavelength from ledger curvature would cite this when partitioning the sphere for solid-angle averaging in the Planck-scale matching. The definition is a direct constant assignment with no computation or lemmas required.
Claim. The number of octants in three-dimensional Euclidean space is $8$.
background
The Planck-Scale Matching module derives λ_rec ≈ 0.564 ℓ_P by equating bit cost J_bit = cosh(ln φ) - 1 to curvature cost J_curv(λ) = 2λ², then restoring SI units via averaging over the eight-face geometry of the Q₃ hypercube. This definition supplies the integer count of octants for that averaging step, which introduces the factor 1/π in the final Planck ratio. Upstream results on spectral emergence establish that Q₃ simultaneously forces three spatial dimensions, the gauge content SU(3) × SU(2) × U(1), and eight local neighbors in the dynamics.
proof idea
The definition is a direct assignment of the constant 8. No lemmas or tactics are applied; the value is hardcoded to match the octant count required by the subsequent solid-angle verification.
why it matters
This definition supplies the integer factor required by the octants_cover_sphere theorem, which confirms that eight octants each subtending π/2 steradians cover the full 4π solid angle. It fills the geometric step in the conjecture C8 derivation, where averaging over the eight-face geometry produces the 1/π factor yielding λ_rec = ℓ_P / √π. The construction aligns with the eight-tick octave and D = 3 forced in the foundational chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.