Encyclopedia Masses Masses Mass Genesis R4 Genesis Route Cdscratch

ARTICLE 5 claims 5 theorems

Masses Mass Genesis R4 Genesis Route Cdscratch

A worker module in the framework's library tests whether rescaling a pattern is a harmless change of units, and finds it is not.

Verify this page

Scaling and the limits of genesis

In the framework's account, a ledger, a discrete record of recognition events, assigns to each stable pattern a number called its rest mass. The module asks a plain question: if you take a pattern and scale it up by a positive factor, do you get the same physics? For a single pattern, the answer is no. The theorem scalePattern_changes_restMass proves that rescaling by any factor other than 1 changes the rest mass, because rest mass is defined as the integrated load on the pattern. A global rescaling of every pattern at once is different: the theorem commonScale_preserves_restMass_ratio proves that mass ratios between two stable patterns survive a common rescaling. That is the only sense in which a global scale could be called a gauge, a freedom to change units without changing observables.

The second charge is sharper. The library defines a carrier certificate: the discrete data, support, topology, and stability flags, that admission structures actually read. A genesis condition is any predicate that agrees on patterns sharing a certificate. The module proves, not assumes, that positive rescaling preserves the certificate (carrierCertificateEq_scalePattern), so every certificate-determined genesis condition is scale-invariant (carrierCertificateGenesis_scaleInvariant). The no-go follows: no such condition that accepts any Q3 carrier can force the target LoadNormalizedToTopology. The theorem carrierCertificateGenesis_does_not_force_loadNormalized states this, and the concrete instance q3MatterCarrier_does_not_force_loadNormalized_of_certificate shows that Q3MatterCarrier itself cannot force it. Two controls prove the class is not empty: LoadNormalizedToTopology and BooleanSettledAnchorWindow are both outside it.

The module is a worker scratch file, not a banked wall. It does not edit the framework's established results. Its value is negative: it rules out a whole family of creation-side conditions as unable to produce the desired per-pattern normalization. The class definition is deliberately non-vacuous, refusing the cheap move of defining the class as scale-invariant; Q3MatterCarrier is inside and does real work. The module closes off a route, and in doing so sharpens what a successful genesis condition would have to look like: it must read absolute magnitudes, not just the certificate.

THEOREM scalePattern_changes_restMass · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
scalePattern_changes_restMass · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:58 
/-- Single-pattern positive rescaling changes rest mass whenever `c ≠ 1`.
Because `restMass` is the observable integrated load on stable patterns, this
map is not a symmetry of everything observable, so it is not gauge in the
sense of `PostingContentGauge`. -/
theorem scalePattern_changes_restMass
    {ψ : LightPattern (Fin 8)} (h : StableClosedLightPattern ψ)
    {c : ℝ} (hc : 0 < c) (hc1 : c ≠ 1) :
    restMass (scalePattern c ψ) ≠ restMass ψ := by
  have hsc : StableClosedLightPattern (scalePattern c ψ) :=
    stableClosedLightPattern_scalePattern (ne_of_gt hc) h
  have hL : 0 < integratedMeaningLoad ψ :=
    integratedMeaningLoad_pos_of_nontrivial ψ h.2.1
  rw [restMass_eq_integratedMeaningLoad_of_stable _ hsc,
    restMass_eq_integratedMeaningLoad_of_stable _ h,
    integratedMeaningLoad_scalePattern]
  intro heq
  have hLne : integratedMeaningLoad ψ ≠ 0 := ne_of_gt hL
  have hsq : c ^ 2 = (1 : ℝ) := by
    have : c ^ 2 * integratedMeaningLoad ψ = (1 : ℝ) * integratedMeaningLoad ψ := by
      rw [one_mul, heq]
    exact (mul_left_inj' hLne).mp this
  have : c = 1 ∨ c = -1 := sq_eq_one_iff.mp hsq
  exact this.elim hc1 (fun hneg => by linarith [hc, hneg])
THEOREM commonScale_preserves_restMass_ratio · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
commonScale_preserves_restMass_ratio · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:82 
/-- Mass ratios between two stable patterns are preserved by a *common* positive
rescaling of both. This is the only sense in which a global scale could be
called gauge. -/
theorem commonScale_preserves_restMass_ratio
    {ψ χ : LightPattern (Fin 8)}
    (hψ : StableClosedLightPattern ψ) (hχ : StableClosedLightPattern χ)
    {c : ℝ} (hc : 0 < c)
    (hχpos : 0 < restMass χ) :
    restMass (scalePattern c ψ) / restMass (scalePattern c χ) =
      restMass ψ / restMass χ := by
  have hsψ : StableClosedLightPattern (scalePattern c ψ) :=
    stableClosedLightPattern_scalePattern (ne_of_gt hc) hψ
  have hsχ : StableClosedLightPattern (scalePattern c χ) :=
    stableClosedLightPattern_scalePattern (ne_of_gt hc) hχ
  rw [restMass_eq_integratedMeaningLoad_of_stable _ hsψ,
    restMass_eq_integratedMeaningLoad_of_stable _ hsχ,
    restMass_eq_integratedMeaningLoad_of_stable _ hψ,
    restMass_eq_integratedMeaningLoad_of_stable _ hχ,
    integratedMeaningLoad_scalePattern, integratedMeaningLoad_scalePattern]
  have hc2 : c ^ 2 ≠ 0 := pow_ne_zero 2 (ne_of_gt hc)
  have hχL : integratedMeaningLoad χ ≠ 0 := by
    rw [← restMass_eq_integratedMeaningLoad_of_stable _ hχ]
    exact ne_of_gt hχpos
  field_simp [hc2, hχL]
THEOREM carrierCertificateEq_scalePattern · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
carrierCertificateEq_scalePattern · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:193 
/-- Positive rescaling preserves the carrier certificate. This is the bridge
from the independently motivated class to scale-invariance. -/
theorem carrierCertificateEq_scalePattern
    {c : ℝ} (hc : 0 < c) (ψ : LightPattern (Fin 8)) :
    CarrierCertificateEq ψ (scalePattern c ψ) := by
  refine ⟨(scalePattern_support c ψ).symm, (scalePattern_topology c ψ).symm, ?_, ?_, ?_⟩
  · constructor
    · exact fun h => stableClosedLightPattern_scalePattern (ne_of_gt hc) h
    · intro h
      have hcinv : (0 : ℝ) < c⁻¹ := inv_pos.mpr hc
      have hψ' : StableClosedLightPattern (scalePattern c⁻¹ (scalePattern c ψ)) :=
        stableClosedLightPattern_scalePattern (ne_of_gt hcinv) h
      rwa [scalePattern_mul_cancel (ne_of_gt hc) ψ] at hψ'
  · simpa using (fullEightTickSupport_scalePattern c ψ).symm
  · simpa using (eightTickWindowEquivariant_scalePattern hc ψ).symm
THEOREM carrierCertificateGenesis_does_not_force_loadNormalized · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
carrierCertificateGenesis_does_not_force_loadNormalized · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:239 
/-- **Main D theorem.** No carrier-certificate genesis condition that accepts a
Q3 carrier can force `LoadNormalizedToTopology` on its accept set. -/
theorem carrierCertificateGenesis_does_not_force_loadNormalized
    (G : LightPattern (Fin 8) → Prop)
    (hG : IsCarrierCertificateGenesisCondition G)
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hacc : G ψ) :
    ¬ ∀ χ : LightPattern (Fin 8), G χ → LoadNormalizedToTopology χ := by
  intro hall
  obtain ⟨χ, hGχ, ⟨Eχ⟩, hratio⟩ :=
    carrierCertificateGenesis_accepts_ratioFour G hG E hacc
  have hnorm : LoadNormalizedToTopology χ := hall χ hGχ
  have hone : loadTopologyRatio χ = 1 :=
    (loadTopologyRatio_eq_one_iff_loadNormalizedToTopology χ).2 hnorm
  have hne : (4 : ℝ) ≠ 1 := by norm_num
  exact hne (hratio.symm.trans hone)
THEOREM q3MatterCarrier_does_not_force_loadNormalized_of_certificate · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
q3MatterCarrier_does_not_force_loadNormalized_of_certificate · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:273 
theorem q3MatterCarrier_does_not_force_loadNormalized_of_certificate :
    ¬ ∀ ψ : LightPattern (Fin 8),
        Q3MatterCarrier ψ → LoadNormalizedToTopology ψ := by
  obtain ⟨E⟩ := q3MatterCarrier_worldlinePattern_gapOne
  exact carrierCertificateGenesis_does_not_force_loadNormalized
    Q3MatterCarrier q3MatterCarrier_isCarrierCertificateGenesis E
    q3MatterCarrier_worldlinePattern_gapOne

What this page does not claim

No claim that any specific genesis condition succeeds in forcing LoadNormalizedToTopology. No claim that the module establishes a positive route to mass generation. No claim about the physical bridge from recognition to observable mass.

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/R4GenesisRouteCDScratch.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND