chirality_product_equals_gap_minus_one
plain-language theorem explainer
The product of the Gray-code chirality flip count on the 3-cube and the CW-filtration torsion gap equals the integration gap minus the active edge count at D=3. Researchers deriving the exact φ-rung for the baryon-to-photon ratio cite this as the chirality-torsion witness among three equivalent combinatorial expressions for the integer -44. The proof substitutes the precomputed integration gap value at three dimensions, unfolds the constants, and evaluates the resulting arithmetic identity.
Claim. At three spatial dimensions, the product of the Gray-code chirality flip count on the 3-cube and the CW-filtration torsion gap between generations equals the integration gap minus the active edge count per fundamental tick: $4 × 11 = 45 - 1$.
background
The module derives the integer -44 that fixes the φ-rung of η_B through three combinatorial witnesses, all equivalent to integrationGap(D) - 1 at D=3. bitFlipCount0 counts the flips of bit 0 on the canonical Gray cycle [0,1,3,2,6,7,5,4] of the 3-cube, yielding 4. torsionGap01 is the absolute difference |11 - 0| drawn from the CW-filtration torsion spectrum {0,11,17}. integrationGap(d) is defined as parityCount(d) times configDim(d) and equals 45 at D=3 by the upstream theorem integrationGap_at_D3. A is the active edge count per tick and equals 1.
proof idea
The proof first applies integrationGap_at_D3 to obtain that the integration gap equals 45 at D=3. It then unfolds bitFlipCount0, torsionGap01, and A to their constant values 4, 11, and 1. A rewrite substitutes the gap value into the target equality, after which the decide tactic confirms the numerical identity 44 = 44.
why it matters
This supplies the chirality-torsion witness for the rung integer -44 and feeds directly into etaBExactRungCert, which assembles the three witnesses and certifies their mutual agreement. The result anchors one combinatorial reparameterization of the integration gap at D=3, which traces to the forcing chain T0-T8 and the Recognition Composition Law. It closes a path in the exact derivation of the η_B rung using only standard kernel facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.