torsion_second
plain-language theorem explainer
The second-generation torsion offset equals 11 in the Recognition Science ledger. Researchers deriving fermion mass ratios from φ-ladder rungs cite this when fixing the rung offset for the second generation. The proof is a one-line simp wrapper that unfolds generationTorsion for the second case together with the passive-field edge count for D=3.
Claim. The torsion offset for the second generation satisfies $τ_2 = 11$, where $τ_2$ is obtained from the passive-field edge count of the D=3 cube.
background
The RSLedger module supplies the rich ledger that places particle masses on discrete rungs of the φ-ladder by adding generation torsion offsets to sector base rungs. Torsion values are derived from D=3 cube combinatorics rather than postulated as φ-formulas. The upstream definition generationTorsion maps the second generation to passive_field_edges D, where passive_field_edges d := cube_edges d - active_edges_per_tick and cube_edges d := d · 2^(d-1) with active_edges_per_tick = 1. The module documentation states that the second generation corresponds to the edge-dressed mode, yielding τ₂ = cube_edges(D) - 1 = 11 for D=3.
proof idea
One-line simp wrapper that unfolds generationTorsion, passive_field_edges, cube_edges, active_edges_per_tick, and D, reducing the claim to a direct numerical identity for the D=3 case.
why it matters
This lemma supplies the concrete value τ₂ = 11 required for the inter-generation mass ratios m₂/m₁ = φ^{11} and m₃/m₂ = φ^6. It realizes the geometric derivation of generation torsion from Q₃ cube edges described in the module documentation and supports the downstream mass formulas on the φ-ladder. The result implements the D=3 requirement of the forcing chain (T8) inside the Recognition Science ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.