Encyclopedia Masses Masses Mass Genesis T10 Pattern Cyclic Shift
ARTICLE 2 claims 2 theorems
Masses Mass Genesis T10 Pattern Cyclic Shift
A machine-checked library proves that shifting a light pattern's clock origin by any number of ticks leaves its predicted mass and recognition cost unchanged.
The cyclic shift test
A cyclic shift moves the starting point of a repeating sequence. Think of a clock face: shifting the origin from 12 to 3 does not change the hour hand's motion, only where you begin reading it. In the Recognition Science framework, a light pattern (a discrete record of eight recognition events) can be shifted the same way. The module called T10 Pattern Cyclic Shift asks whether this coordinate choice matters for physics. The answer, proved in a machine-checked library of formal theorems, is that it does not: shifting the clock origin leaves the pattern's predicted mass, rest mass, and recognition cost exactly unchanged.
The framework models matter as stable patterns of recognition events. A recognition cost (a forced expense associated with each event) is assigned to each pattern. The core question is whether this cost depends on where you start counting. The theorem loadRecognitionCost_simultaneousCyclicShift proves that applying the same shift to every site window leaves the cost identical. The proof is short and direct: it unfolds the definition of cost and rewrites using the fact that shifting preserves the topology ratio. The same invariance holds for predicted mass (predictedMass_simultaneousCyclicShift) and for rest mass when the pattern is stable (restMass_simultaneousCyclicShift_of_stable).
This invariance is not trivial. The framework's eight-tick cycle means a shift by one tick changes which events land in which window. Yet the mass and cost do not change. The module also builds quotient infrastructure: it defines an equivalence relation identifying patterns that evolve into each other, and proves this relation is an equivalence. Two specific patterns, gapOne and gapTwo, are shown to be genuinely different even under this equivalence (gapOne_patternRHatQuotient_ne_gapTwo). So the shift invariance is not collapsing distinct matter states into one; it only removes the arbitrary choice of where the clock starts.
What this establishes in plain language: the framework's mass predictions are coordinate-invariant under time translation. If you relabel the ticks, you get the same physics. This is a necessary consistency check for any theory that claims to derive particle masses from a discrete ledger. The module does not yet derive the actual settled mass values, nor does it prove matter uniqueness. It certifies that the foundation is stable under a basic symmetry, which is the first step before any mass prediction can be trusted.
THEOREM loadRecognitionCost_simultaneousCyclicShift · predictedMass_simultaneousCyclicShift · restMass_simultaneousCyclicShift_of_stable · IndisputableMonolith/Masses/MassGenesis/T10PatternCyclicShift.lean
/-- Pattern load-recognition cost is independent of clock origin. -/
theorem loadRecognitionCost_simultaneousCyclicShift
(ψ : LightPattern (Fin 8))
(k : Fin 8) :
loadRecognitionCost (simultaneousCyclicShift k ψ) =
loadRecognitionCost ψ := by
unfold loadRecognitionCost
rw [loadTopologyRatio_simultaneousCyclicShift]
/-- The topology-predicted mass is independent of clock origin. -/
theorem predictedMass_simultaneousCyclicShift
(ψ : LightPattern (Fin 8))
(k : Fin 8) :
predictedMass (simultaneousCyclicShift k ψ) = predictedMass ψ :=
rfl
/-- Stable rest mass is independent of clock origin. -/
theorem restMass_simultaneousCyclicShift_of_stable
(ψ : LightPattern (Fin 8))
(k : Fin 8)
(h : StableClosedLightPattern ψ) :
restMass (simultaneousCyclicShift k ψ) = restMass ψ :=
restMass_evolvePattern_of_stable ψ k.val h
THEOREM gapOne_patternRHatQuotient_ne_gapTwo · IndisputableMonolith/Masses/MassGenesis/T10PatternCyclicShift.lean
/-- Gap one and gap two define different full-pattern quotient points. -/
theorem gapOne_patternRHatQuotient_ne_gapTwo :
Quotient.mk patternRHatOrbitSetoid
(worldlinePattern gapOneTwoPhaseMode) ≠
Quotient.mk patternRHatOrbitSetoid
(worldlinePattern gapTwoTwoPhaseMode) := by
intro h
exact gapOne_not_patternRHatOrbitEquivalent_gapTwo
(Quotient.exact h)
What this page does not claim
The module does not derive the physical settled mass readout or matter uniqueness. The shift invariance does not imply that all patterns with the same mass are physically identical. The framework's cyclic shift is a coordinate choice, not a physical rotation in space.
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/T10PatternCyclicShift.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 physical mass values do the stable light patterns actually predict?
- How does the shift invariance connect to the framework's derivation of three spatial dimensions?
- What distinguishes the gapOne and gapTwo patterns beyond their non-equivalence under cyclic shift?
- Does the quotient construction extend to a full classification of all stable matter patterns?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM loadRecognitionCost_simultaneousCyclicShift · predictedMass_simultaneousCyclicShift · restMass_simultaneousCyclicShift_of_stable · IndisputableMonolith/Masses/MassGenesis/T10PatternCyclicShift.lean
/-- Pattern load-recognition cost is independent of clock origin. -/ theorem loadRecognitionCost_simultaneousCyclicShift (ψ : LightPattern (Fin 8)) (k : Fin 8) : loadRecognitionCost (simultaneousCyclicShift k ψ) = loadRecognitionCost ψ := by unfold loadRecognitionCost rw [loadTopologyRatio_simultaneousCyclicShift]/-- The topology-predicted mass is independent of clock origin. -/ theorem predictedMass_simultaneousCyclicShift (ψ : LightPattern (Fin 8)) (k : Fin 8) : predictedMass (simultaneousCyclicShift k ψ) = predictedMass ψ := rfl/-- Stable rest mass is independent of clock origin. -/ theorem restMass_simultaneousCyclicShift_of_stable (ψ : LightPattern (Fin 8)) (k : Fin 8) (h : StableClosedLightPattern ψ) : restMass (simultaneousCyclicShift k ψ) = restMass ψ := restMass_evolvePattern_of_stable ψ k.val hshifting the clock origin leaves the pattern's predicted mass, rest mass, and recognition cost exactly unchanged loadRecognitionCost_simultaneousCyclicShift · predictedMass_simultaneousCyclicShift · restMass_simultaneousCyclicShift_of_stable · IndisputableMonolith/Masses/MassGenesis/T10PatternCyclicShift.leanTHEOREM gapOne_patternRHatQuotient_ne_gapTwo · IndisputableMonolith/Masses/MassGenesis/T10PatternCyclicShift.lean
/-- Gap one and gap two define different full-pattern quotient points. -/ theorem gapOne_patternRHatQuotient_ne_gapTwo : Quotient.mk patternRHatOrbitSetoid (worldlinePattern gapOneTwoPhaseMode) ≠ Quotient.mk patternRHatOrbitSetoid (worldlinePattern gapTwoTwoPhaseMode) := by intro h exact gapOne_not_patternRHatOrbitEquivalent_gapTwo (Quotient.exact h)Two specific patterns, gapOne and gapTwo, are shown to be genuinely different even under this equivalence gapOne_patternRHatQuotient_ne_gapTwo · IndisputableMonolith/Masses/MassGenesis/T10PatternCyclicShift.lean