localCoeff
The local coefficient supplies the cellwise ratio of k-cell count to anchoring vertices per cell in the 3-cube geometry. Researchers deriving first-principles lepton mass corrections would cite it to obtain the facet-mediated term without external fitting. It is realized as the direct quotient of the cellCount and anchorsPerCell functions at the input dimension k.
claimFor each cell dimension $k$ (vertex, edge, face or cube) in the 3-cube, the local coefficient is the ratio $N_k / A_k$, where $N_k$ is the number of $k$-cells and $A_k$ is the number of vertices anchoring each $k$-cell.
background
This module derives the dimension-dependent correction Δ(D) = D/2 from cube geometry without calibration to observed masses. The goal is to show that Δ(3) = 3/2 is forced by the framework. The deep analogy contrasts the e→μ step (edge-mediated via continuous solid angle 4π) with the μ→τ step (facet-mediated via discrete vertex count as solid-angle analog).
proof idea
This is a direct definition that computes the ratio of cellCount k to anchorsPerCell k after casting both to reals. No auxiliary lemmas are invoked; the body simply performs the division using the already-defined cellCount and anchorsPerCell maps on CellDim.
why it matters in Recognition Science
It is invoked by the downstream theorems localCoeff_face (yielding exactly 3/2), localCoeff_eq_three_halves_iff (uniqueness inside the admissible local mechanism class), and the face-ne-edge and face-ne-cube inequalities. This supplies the concrete geometric value for the facet-mediated correction in the μ→τ lepton step, consistent with the Recognition Science forcing chain at T8 (D = 3) and the Recognition Composition Law.
scope and limits
- Does not extend the ratio to spatial dimensions other than 3.
- Does not incorporate continuous measures such as solid angles.
- Does not depend on observed particle masses or coupling constants.
- Does not define the global Δ(D) correction, only the local cellwise version.
- Does not address multi-step interactions or higher-order terms.
Lean usage
theorem localCoeff_face_example : localCoeff .face = 3/2 := by unfold localCoeff; norm_numformal statement (Lean)
317noncomputable def localCoeff (k : CellDim) : ℝ :=
proof body
Definition body.
318 (cellCount k : ℝ) / (anchorsPerCell k : ℝ)
319