localCoeff_cube
plain-language theorem explainer
The theorem establishes that the normalized local coefficient for the three-dimensional cube cell equals one eighth. Researchers deriving the facet-mediated correction in the muon-to-tau lepton transition from first principles would cite this when isolating the discrete vertex contribution. The proof is a direct term-mode computation that unfolds the cell-count and anchor-per-cell definitions then evaluates the ratio via normalization.
Claim. Let the local coefficient for a cell dimension be the ratio of the number of cells of that dimension to the number of anchoring vertices per cell. For the cube (three-cell) this ratio equals $1/8$.
background
The module derives the dimension-dependent correction Δ(D) = D/2 from cube geometry without calibration to observed masses, modeling the μ→τ step as facet-mediated. Cell count assigns one cube, six faces, twelve edges and eight vertices; anchors per cell assigns eight vertices to each cube, four to each face, two to each edge and one to each vertex. The local coefficient is then the ratio of these two quantities, supplying the discrete analog of solid angle via vertex count. The admissible predicate from information thermodynamics is the trivial predicate True on any ledger state, serving as the interface for local dissipative recognition operators.
proof idea
The proof unfolds the definitions of the local coefficient, cell count and anchors per cell at the cube case, then applies norm_num to reduce the resulting rational arithmetic directly to the value 1/8.
why it matters
This supplies the cube value required by the sibling theorem establishing that the face coefficient differs from the cube coefficient, thereby isolating the 3/2 cross-level ratio for the facet-mediated correction. It fills the concrete geometric step in the module's first-principles derivation of Δ(3) = 3/2, consistent with the framework's forcing of three spatial dimensions. The result sharpens the analogy between continuous solid angle in the edge-mediated step and discrete vertex count in the facet-mediated step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.