discrete_continuous_duality
plain-language theorem explainer
The duality theorem equates the electron-muon transition contribution of 1 over 4 pi to the muon-tau transition contribution of 6 over 4, with the discrete face measure fixed at 4 vertices. Researchers deriving lepton mass ladders from cube geometry cite it to establish the dimension-dependent correction without empirical fitting. The proof proceeds by direct term construction, reflexivity on the continuous and vertex definitions, and numerical reduction after unfolding the face-count and vertex-count auxiliaries.
Claim. The continuous-discrete duality asserts that the electron-to-muon contribution equals $1/(4pi)$, the muon-to-tau contribution equals $6/4$, and the discrete measure for a two-dimensional face equals 4.
background
The module derives the dimension-dependent correction Delta(D) = D/2 from cube geometry without calibration to observed masses. It contrasts the e to mu step, which uses the continuous solid-angle measure 4 pi for the active-edge contribution 1 over 4 pi, with the mu to tau step, which uses the discrete vertex count V as the normalization for the facet contribution F over V. The vertex count is the discrete analog of the solid angle: each facet contributes 1 over V where V equals 2 to the power D minus 1, yielding Delta equals 3 over 2 at D equals 3. Upstream structures supply the active-edge count A equals 1 and the J-cost definitions that anchor the underlying forcing chain.
proof idea
The term proof constructs the three-way conjunction by reflexivity on the first and third conjuncts. For the middle conjunct it unfolds the definitions of muTauContribution, discreteMeasure2DFace, faceCount and faceVertexCount, then applies numerical normalization to reduce the ratio to 6 over 4.
why it matters
This theorem anchors the first-principles derivation of Delta(D) equals D over 2 inside the lepton-generations module. It supplies the discrete-continuous duality that parallels the continuous solid-angle factor 1 over 4 pi with the discrete vertex factor 1 over 4, thereby supporting the Recognition Science claim that lepton masses arise from phi-ladder steps. The result connects to the T8 forcing of three spatial dimensions and the Recognition Composition Law through the J-cost structures that generate the underlying ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.