Masses Mass Genesis Master Certificate

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

/-- **N4 route (a) result.** On the carrier, the load-normalization residual is exactly
the vanishing of the canonical recognition cost of the load-to-topology ratio: the σ = 0
ledger-balance condition. -/
theorem loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology
    {ψ : LightPattern (Fin 8)} (E : Q3ClosedPatternEvidence ψ) :
    loadRecognitionCost ψ = 0 ↔ LoadNormalizedToTopology ψ := by
  unfold loadRecognitionCost
  rw [IndisputableMonolith.Cost.Jcost_eq_zero_iff _
    (loadTopologyRatio_pos_of_q3ClosedEvidence E)]
  exact loadTopologyRatio_eq_one_iff_loadNormalizedToTopology ψ

/-- **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

/-- 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, BALANCE source vs O3 window-residual, sess. 12).**
The BALANCE source cannot supply window-equivariance even on its eigenvalue-1 eigenspace.
Every window of `constWindowPattern gapOneTwoPhaseMode` is BALANCE-fixed
(`neutralize w = w`, since the gap-1 window is already neutral), so the whole pattern lives
in the fixed-point set `{ψ | P ψ = ψ}` of the BALANCE projection — yet it is not
`EightTickWindowEquivariant`. Combined with `neutralize_cyclicShift_comm` (BALANCE commutes
with R̂, hence preserves the equivariance class), this shows BALANCE — the first-listed
dynamical source, with its proven `P² = P` / self-adjoint spectral structure — provably does
NOT force the worldline identification. All four named sources (BALANCE here; R̂-orbit and
spatial closure in `spatiallyClosedStable_does_not_force_windowEquivariant`) are now closed
against the window residual. -/
theorem balanceFixed_does_not_force_windowEquivariant :
    (∀ x, neutralize ((constWindowPattern gapOneTwoPhaseMode).window x)
        = (constWindowPattern gapOneTwoPhaseMode).window x) ∧
      ¬ EightTickWindowEquivariant (constWindowPattern gapOneTwoPhaseMode) := by
  refine ⟨fun x => ?_, fullSupport_does_not_force_windowEquivariant.2⟩
  show neutralize gapOneTwoPhaseMode = gapOneTwoPhaseMode
  funext j
  show gapOneTwoPhaseMode j - (∑ i, gapOneTwoPhaseMode i) / 8 = gapOneTwoPhaseMode j
  rw [gapOneTwoPhaseMode_neutral]; ring