Encyclopedia Masses Masses Mass Genesis T10 Octave Settlement Readout Parity Octave Corner Window Eq
ARTICLE 4 claims 4 theorems
Masses Mass Genesis T10 Octave Settlement Readout Parity Octave Corner Window Eq
A parity-signed sum of eight phase windows vanishes at exactly two of the eight ticks, and that precise vanishing pattern is what the framework's machine-checked library proves.
The parity-signed octave readout
In the Recognition Science framework, the eight ticks of a cycle each carry a phase posting, and a window (a function assigning a complex number to each tick) records how strongly a posting registers at that tick. The declaration parityOctaveCornerWindow_eq_zero_iff establishes an exact fact about one such window: the parity-signed octave sum, which adds the eight phase windows with alternating signs (plus, minus, plus, minus, and so on around the cycle). The theorem states that this parity-signed sum equals zero at a tick if and only if that tick is tick zero or tick five.
The content is precise and narrow. It does not say the sum is zero at other ticks, nor that it is nonzero everywhere else; it gives the exact two-element set of zeros. The proof, checked by the framework's machine-checked library of formal theorems, works by evaluating the sum at each of the eight ticks and showing that the complex number at tick zero and tick five simplifies to zero, while at each of the other six ticks the number is forced to be nonzero by the algebraic properties of the underlying torus root. The theorem also carries a companion result: the parity-signed sum is nontrivial (not identically zero) and is compatible with the physical photon window condition, meaning it behaves like a legitimate readout rather than a degenerate one.
The significance lies in what the vanishing pattern rules out. The framework's docstring explains that a plain (un-signed) octave sum is nonzero at every tick, so it cannot supply raw support for the two-phase output that the settlement mechanism needs. The parity-signed version is sharper: its zeros at exactly tick zero and tick five mean its support is the other six ticks, the mixed-vertex ones in the Gray-code picture. The theorem therefore proves that neither plain nor parity-signed superposition of single-posting corner readouts produces the desired concentration onto phases zero and one. The residual two-phase output, if it exists, must come from a different settlement mechanism, not from this superposition.
What the declaration does not claim is equally important. It does not assert that the parity-signed sum is the settlement mechanism itself, nor that any physical mass value follows from it. It establishes only the algebraic vanishing pattern of one constructed window. The framework's own description marks the window as a canonical model construction, with no weight chosen to shape the target, and the stated property as a theorem about that construction. The step from this readout pattern to actual mass genesis, the physical bridge, remains open in the framework; the theorem is a necessary condition, not a sufficient one. A reader should take it as a precise structural fact about a defined object, not as a derivation of particle masses.
THEOREM parityOctaveCornerWindow_eq_zero_iff · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.lean
/-- **Zero-set characterization.** The parity-signed settled readout vanishes
exactly at the two ticks whose Gray vertex is uniform: all-false at tick zero
and all-true at tick five. -/
theorem parityOctaveCornerWindow_eq_zero_iff (t : Fin 8) :
parityOctaveCornerWindow t = 0 ↔ t = 0 ∨ t = 5 := by
constructor
· intro h
fin_cases t
· exact Or.inl rfl
· exact absurd h parity_ne_one
· exact absurd h parity_ne_two
· exact absurd h parity_ne_three
· exact absurd h parity_ne_four
· exact Or.inr rfl
· exact absurd h parity_ne_six
· exact absurd h parity_ne_seven
· rintro (rfl | rfl)
· exact parityVal_zero
· exact parityVal_five
THEOREM parityOctaveCornerWindow_nontrivial · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.lean
theorem parityOctaveCornerWindow_nontrivial :
PhotonWindow.nontrivial parityOctaveCornerWindow :=
⟨1, parity_ne_one⟩
THEOREM parityOctaveCornerWindow_currentPhysicalPhotonWindowCompatible · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.lean
/-- **Admissibility.** The parity-signed settled readout is a physically
compatible photon window: nontrivial with nonzero neutralized energy. The
settled octave does post an admissible window, derived from the source. -/
theorem parityOctaveCornerWindow_currentPhysicalPhotonWindowCompatible :
CurrentPhysicalPhotonWindowCompatible parityOctaveCornerWindow := by
refine ⟨parityOctaveCornerWindow_nontrivial, ?_⟩
have hneutral : IsNeutral parityOctaveCornerWindow :=
parityOctaveCornerWindow_neutral
rw [LightLanguage.Geometry.NeutralMeaningManifold.neutralize_of_neutral
parityOctaveCornerWindow hneutral]
intro hzero
have hall :=
(Finset.sum_eq_zero_iff_of_nonneg
(fun i _ => Complex.normSq_nonneg (parityOctaveCornerWindow i))).mp
(by simpa [normSq8] using hzero) 1 (Finset.mem_univ 1)
exact parity_ne_one (Complex.normSq_eq_zero.mp hall)
THEOREM parityOctaveCornerWindow_not_rawPhotonPhase01Support · octaveCornerWindow_not_rawPhotonPhase01Support · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.lean
theorem parityOctaveCornerWindow_not_rawPhotonPhase01Support :
¬ RawPhotonPhase01Support parityOctaveCornerWindow := fun h =>
parity_ne_two (h 2 (by decide) (by decide))
theorem octaveCornerWindow_not_rawPhotonPhase01Support :
¬ RawPhotonPhase01Support octaveCornerWindow := fun h =>
octaveCornerWindow_ne_zero 2 (h 2 (by decide) (by decide))
What this page does not claim
The parity-signed sum is the settlement mechanism itself. Any particle mass value follows from this vanishing pattern. The physical bridge from this readout to mass genesis is established.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What settlement mechanism, if any, produces the two-phase output that this readout pattern rules out?
- How does the vanishing pattern at ticks zero and five relate to the Gray-code vertex structure?
- What physical content, if any, does the framework attach to the two-phase output beyond the algebraic pattern?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM parityOctaveCornerWindow_eq_zero_iff · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.lean
/-- **Zero-set characterization.** The parity-signed settled readout vanishes exactly at the two ticks whose Gray vertex is uniform: all-false at tick zero and all-true at tick five. -/ theorem parityOctaveCornerWindow_eq_zero_iff (t : Fin 8) : parityOctaveCornerWindow t = 0 ↔ t = 0 ∨ t = 5 := by constructor · intro h fin_cases t · exact Or.inl rfl · exact absurd h parity_ne_one · exact absurd h parity_ne_two · exact absurd h parity_ne_three · exact absurd h parity_ne_four · exact Or.inr rfl · exact absurd h parity_ne_six · exact absurd h parity_ne_seven · rintro (rfl | rfl) · exact parityVal_zero · exact parityVal_fivethe parity-signed octave sum equals zero at a tick if and only if that tick is tick zero or tick five parityOctaveCornerWindow_eq_zero_iff · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.leanTHEOREM parityOctaveCornerWindow_nontrivial · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.lean
theorem parityOctaveCornerWindow_nontrivial : PhotonWindow.nontrivial parityOctaveCornerWindow := ⟨1, parity_ne_one⟩the parity-signed sum is nontrivial (not identically zero) parityOctaveCornerWindow_nontrivial · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.leanTHEOREM parityOctaveCornerWindow_currentPhysicalPhotonWindowCompatible · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.lean
/-- **Admissibility.** The parity-signed settled readout is a physically compatible photon window: nontrivial with nonzero neutralized energy. The settled octave does post an admissible window, derived from the source. -/ theorem parityOctaveCornerWindow_currentPhysicalPhotonWindowCompatible : CurrentPhysicalPhotonWindowCompatible parityOctaveCornerWindow := by refine ⟨parityOctaveCornerWindow_nontrivial, ?_⟩ have hneutral : IsNeutral parityOctaveCornerWindow := parityOctaveCornerWindow_neutral rw [LightLanguage.Geometry.NeutralMeaningManifold.neutralize_of_neutral parityOctaveCornerWindow hneutral] intro hzero have hall := (Finset.sum_eq_zero_iff_of_nonneg (fun i _ => Complex.normSq_nonneg (parityOctaveCornerWindow i))).mp (by simpa [normSq8] using hzero) 1 (Finset.mem_univ 1) exact parity_ne_one (Complex.normSq_eq_zero.mp hall)the parity-signed sum is compatible with the physical photon window condition parityOctaveCornerWindow_currentPhysicalPhotonWindowCompatible · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.leanTHEOREM parityOctaveCornerWindow_not_rawPhotonPhase01Support · octaveCornerWindow_not_rawPhotonPhase01Support · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.lean
theorem parityOctaveCornerWindow_not_rawPhotonPhase01Support : ¬ RawPhotonPhase01Support parityOctaveCornerWindow := fun h => parity_ne_two (h 2 (by decide) (by decide))theorem octaveCornerWindow_not_rawPhotonPhase01Support : ¬ RawPhotonPhase01Support octaveCornerWindow := fun h => octaveCornerWindow_ne_zero 2 (h 2 (by decide) (by decide))neither plain nor parity-signed superposition of single-posting corner readouts produces the desired concentration onto phases zero and one parityOctaveCornerWindow_not_rawPhotonPhase01Support · octaveCornerWindow_not_rawPhotonPhase01Support · IndisputableMonolith/Masses/MassGenesis/T10OctaveSettlementReadout.lean