Masses Mass Genesis Master Certificate Full Mass Genesis Conclusion Of Stable Cl

/-- On the Q3 carrier, the load-normalization residual forces the mass law. Combined
with `restMass_eq_predictedMass_iff_canonicalPrimitiveLoadFactorizes`, this localizes
the residual to exactly the physical mass-law input. -/
theorem loadNormalizedToTopology_forces_massLaw
    {ψ : LightPattern (Fin 8)} (E : Q3ClosedPatternEvidence ψ)
    (h : LoadNormalizedToTopology ψ) :
    restMass ψ = predictedMass ψ :=
  (restMass_eq_predictedMass_iff_canonicalPrimitiveLoadFactorizes E.stable).2
    (canonicalPrimitiveLoadFactorizes_of_loadNormalizedToTopology E h)

/-- M1 on the carrier in σ = 0 form: the full Mass Genesis conclusion holds when the
load-ratio recognition cost vanishes. This is route (a)'s closure of the carrier
theorem onto the canonical RS ledger. -/
theorem massGenesisOnCarrier_of_loadRecognitionCost_zero
    (T : StableLoadReadoutTheory (Fin 8))
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hcost : loadRecognitionCost ψ = 0) :
    (∀ k : ℕ,
      integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
    0 < restMass ψ ∧
    PhiRungQuantized ψ ∧
    restMass ψ = predictedMass ψ ∧
    T.readout.inertialMass ψ = restMass ψ ∧
    T.readout.gravitationalMass ψ = restMass ψ :=
  massGenesisOnCarrier_of_loadNormalizedToTopology T ⟨E⟩
    ((loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology E).1 hcost)

/-- **OBSTRUCTION (carrier dynamics, O3 window-residual, sess. 11).** The window-equivariance
hypothesis of `massGenesisOnSpatiallyClosedStable_of_residuals` is genuinely INDEPENDENT of its
spatial-closure source — it cannot be dropped, and no genuine Q3-closure dynamical source supplies it.
The constant pattern on the gap-1 neutral window is a FULL `SpatiallyClosedStablePattern`: its support
is all of `Fin 8` (localized and trivially step-closed, hence `FullEightTickSupport`), it carries
nontrivial neutral load (`normSq8 (neutralize gapOneTwoPhaseMode) = 2 > 0`), and it closes under the
R̂-orbit at period 8 (`cyclicShift_period_8`). Yet it FAILS `EightTickWindowEquivariant`, because every
site carries the SAME window rather than successive `cyclicShift` images, and the gap-1 window is not
R̂-fixed. So the three genuine closure sources combined — R̂-orbit closure (`ClosedRHatOrbit`), spatial
step-closure (`SpatialStepClosedSupport`), and stability — do not force window-equivariance. It is
irreducibly the worldline identification of one site-step with one R̂-tick, a separate dynamical input.
This strengthens the session-8 `fullSupport_does_not_force_windowEquivariant` (which only used full
SITE support) to the full carrier-source predicate. -/
theorem spatiallyClosedStable_does_not_force_windowEquivariant :
    SpatiallyClosedStablePattern (constWindowPattern gapOneTwoPhaseMode) ∧
      ¬ EightTickWindowEquivariant (constWindowPattern gapOneTwoPhaseMode) := by
  refine ⟨⟨⟨?_, ?_, ?_⟩, ?_⟩, fullSupport_does_not_force_windowEquivariant.2⟩
  · exact Finset.univ_nonempty
  · refine ⟨0, Finset.mem_univ _, ?_⟩
    have hneut : neutralize ((constWindowPattern gapOneTwoPhaseMode).window 0)
        = gapOneTwoPhaseMode := by
      funext j
      show gapOneTwoPhaseMode j - (∑ i, gapOneTwoPhaseMode i) / 8 = gapOneTwoPhaseMode j
      rw [gapOneTwoPhaseMode_neutral]; ring
    rw [hneut]
    have hns : normSq8 gapOneTwoPhaseMode = 2 := by
      simp [normSq8, gapOneTwoPhaseMode, Fin.sum_univ_eight, Complex.normSq_apply]; norm_num
    rw [hns]; norm_num
  · exact ⟨8, by norm_num, dvd_refl 8, fun x _ => cyclicShift_period_8 _⟩
  · intro x _; exact Finset.mem_univ _

/-- **OBSTRUCTION (carrier dynamics, sess. 21).** The σ = 0 principle does NOT force
`LocalizedSupport` (support nonemptiness). `loadRecognitionCost` depends only on the anchor
window and the topology (both `normSq8 (neutralize (ψ.window 0))` and
`primitiveClosedPatternAmplitude ψ` ignore the support Finset), so emptying the support of the
sess. 20 witness preserves `loadRecognitionCost = 0` while destroying `LocalizedSupport`. Hence
the existence of a localized (and, by the same reasoning, R̂-orbit-closed) pattern is genuinely
NOT supplied by the σ = 0 principle: it is the irreducible existence-of-matter postulate that
the `SpatiallyClosedStablePattern` source encodes. This pins the architecture's final boundary:
σ = 0 supplies the anchor load magnitude; the existence of a closed stable orbit is the separate
physical input. -/
theorem sigmaZero_does_not_force_localizedSupport :
    ∃ ψ : LightPattern (Fin 8),
      loadRecognitionCost ψ = 0 ∧ ¬ LocalizedSupport ψ := by
  obtain ⟨ψ, _, _, hσ⟩ := exists_massGenesisCapstone_sigmaZeroBoth_witness
  refine ⟨emptySupportPattern ψ, ?_, ?_⟩
  · show loadRecognitionCost (emptySupportPattern ψ) = 0
    exact hσ
  · show ¬ (emptySupportPattern ψ).support.Nonempty
    simp [emptySupportPattern]

theorem refined_mass_genesis_stable_pattern_gives_masslaw
    {ψ : LightPattern (Fin 8)}
    (hψ : RefinedMassGenesisStablePattern ψ) :
    restMass ψ = predictedMass ψ :=
  restMass_eq_predictedMass_of_primitiveMassGenesisDynamics hψ

/-- **THEOREM (N4 route (a) achievability, uniqueness, sess. 16).** The σ = 0 ground state
is UNIQUE in each carrier's positive-scale orbit: if two positive scales both normalize the
load to topology, they coincide. Together with `exists_scale_loadNormalizedToTopology` this
gives the full variational characterization — every carrier scale-orbit contains exactly one
recognition-cost ground state, the unique J-cost minimizer. The only physical input left for
the load residual is the σ = 0 postulate (matter IS that minimizer), which is now proved both
non-vacuous and unique rather than assumed. -/
theorem unique_scale_loadNormalizedToTopology
    {ψ : LightPattern (Fin 8)} (E : Q3ClosedPatternEvidence ψ)
    {c c' : ℝ} (hc : 0 < c) (hc' : 0 < c')
    (h : LoadNormalizedToTopology (scalePattern c ψ))
    (h' : LoadNormalizedToTopology (scalePattern c' ψ)) :
    c = c' := by
  have key : ∀ d : ℝ, LoadNormalizedToTopology (scalePattern d ψ) →
      d ^ 2 * normSq8 (neutralize (ψ.window 0))
        = primitiveClosedPatternAmplitude ψ ^ 2 := by
    intro d hd
    unfold LoadNormalizedToTopology AnchorPhasePrimitiveAmplitudeNorm at hd
    have hwin : (scalePattern d ψ).window 0 = (fun t => (d : ℂ) * (ψ.window 0) t) := rfl
    have hamp : primitiveClosedPatternAmplitude (scalePattern d ψ)
        = primitiveClosedPatternAmplitude ψ := rfl
    rw [hwin, normSq8_neutralize_smul, hamp] at hd
    exact hd
  have hL0pos : 0 < normSq8 (neutralize (ψ.window 0)) :=
    site0_neutralLoad_pos_of_q3ClosedEvidence E
  have hsq : c ^ 2 = c' ^ 2 :=
    mul_right_cancel₀ (ne_of_gt hL0pos) (by rw [key c h, key c' h'])
  have hfac : (c - c') * (c + c') = 0 := by linear_combination hsq
  rcases mul_eq_zero.1 hfac with h1 | h2
  · linarith
  · exfalso; linarith

/-- **THEOREM (Lane E, fermionicity is not forced).** There is a window that is neutral
(`∑ = 0`), fixed by four recognition ticks (`P⁴ = +I`, integer spin), yet outside the fermion
core. Hence neither neutrality nor shift-closure forces `HalfIntegerWindow`: the bosonic sector is
nonempty and equally admissible, so selecting the spin-½ (matter) sector is a genuine physical
input, the residual-2 analogue of N4's "topology cannot force the absolute scale." -/
theorem fermionicity_not_forced :
    ∃ w : Fin 8 → ℂ,
      w ∈ neutralRegister ∧ cyclicShiftIter 4 w = w ∧ w ∉ quarterTurnCore := by
  refine ⟨dft8_mode (2 : Fin 8), ?_, shiftFour_fixes_mode_two,
    dft8_mode_two_not_mem_quarterTurnCore⟩
  exact dft8_mode_mem_neutralRegister (by decide)