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

current_chain_endpoints

show as:
view Lean formalization →

The endpoints of the current generation-step chain sum to 21. Researchers enumerating phi-ladder mass values under Q3 cube invariants cite this arithmetic constraint when partitioning N3 = 55 with middle sum 17. The proof is a one-line numerical normalization that directly verifies the addition.

claimThe sum of the endpoint values in the current generation chain is $13 + 8 = 21$.

background

The module narrows the gap between proved Q3 cell counts and their identification as generation steps. The four values {13, 11, 6, 8} arise as cube invariants at D=3: 13 from Euler characteristic V-E+F=2 on the boundary, 11 as passive edges, 6 as faces, and 8 as vertices. The endpoint pair must satisfy the partition constraint with middle pair summing to 17, yielding the total 21. Upstream structures supply the J-cost convexity from PhiForcingDerived and the spectral emergence of exactly three generations from SpectralEmergence.

proof idea

The proof is a one-line term that applies norm_num to confirm the arithmetic identity 13 + 8 = 21.

why it matters in Recognition Science

This records the endpoint sum constraint required for the uniqueness argument in current_chain_unique_modulo_edge_pair_filter. It advances the step-value enumeration that narrows the open forcing step identified in SectorDependentTorsion, making the modeling choice of natural cube invariants explicit. The result sits inside the T5-T8 forcing chain where phi and the eight-tick octave fix the discrete structure before mass assignment on the phi-ladder.

scope and limits

formal statement (Lean)

 139theorem current_chain_endpoints : 13 + 8 = 21 := by norm_num

proof body

Term-mode proof.

 140
 141/-- All four values of the current chain are distinct. -/

depends on (5)

Lean names referenced from this declaration's body.