pith. machine review for the scientific record. sign in
theorem proved term proof high

localCoeff_cube

show as:
view Lean formalization →

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.

claimLet 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 332theorem localCoeff_cube : localCoeff .cube = 1 / 8 := by

proof body

Term-mode proof.

 333  unfold localCoeff cellCount anchorsPerCell
 334  norm_num
 335
 336/-! ### Uniqueness inside the admissible local mechanism class -/
 337
 338/-- Within the local (cellwise) mechanism class, **only** face-mediation yields 3/2 in the 3-cube. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.