Encyclopedia Masses Masses Mass Genesis R4 Genesis Route Cdscratch Load Normalized To Topology Not C

ARTICLE 5 claims 5 theorems

Masses Mass Genesis R4 Genesis Route Cdscratch Load Normalized To Topology Not C

A machine-checked proof shows that a natural way to define which patterns become matter cannot, by itself, force the mass-to-topology ratio the framework seeks.

Verify this page

The certificate boundary

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition is the act of matching a new event against that record. The declaration loadNormalizedToTopology_not_carrierCertificateGenesis is a theorem in the framework's machine-checked library of formal theorems. It states that a specific property, called LoadNormalizedToTopology, is not determined by what the library calls a carrier certificate.

A carrier certificate is a package of discrete facts about a pattern: its support, its topology, whether it is a stable closed light pattern, whether it has full eight-tick support, and whether it is eight-tick window equivariant. The theorem proves that two patterns can share all these certificate fields and yet disagree on whether they satisfy LoadNormalizedToTopology. In plainer terms, knowing the certificate does not tell you the load-to-topology ratio. The ground state and its doubled rescaling are the concrete example: both are Q3 matter carriers with the same support and topology, but they differ on the target property.

The result is a no-go theorem for a whole class of genesis conditions. A genesis condition is a rule for admitting patterns as matter. The class in question, IsCarrierCertificateGenesisCondition, contains any rule that gives the same verdict to patterns with equal carrier certificates. The theorem proves that no such rule, if it accepts any Q3 carrier, can force LoadNormalizedToTopology on everything it accepts. The proof works by rescaling: positive rescaling preserves the certificate, so a doubled carrier is always available to break the target property.

This is not a failure of the framework. It is a precise boundary. The theorem does not claim that mass genesis is impossible, only that this particular certificate-based route cannot reach the target on its own. It also does not claim that rescaling is a gauge symmetry in general: a single-pattern rescaling changes rest mass, which is an observable. Only a common rescaling of two patterns preserves their mass ratio. The result leaves open whether another class of conditions, using different fields, could force the target.

THEOREM loadNormalizedToTopology_not_carrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
loadNormalizedToTopology_not_carrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:283 
/-- `LoadNormalizedToTopology` is outside the class: the ground state and its
double share a carrier certificate (both are Q3 carriers with the same support
and topology) but disagree on the target. -/
theorem loadNormalizedToTopology_not_carrierCertificateGenesis :
    ¬ IsCarrierCertificateGenesisCondition LoadNormalizedToTopology := by
  intro hG
  obtain ⟨Eseed⟩ := q3MatterCarrier_worldlinePattern_gapOne
  obtain ⟨c, hc, hground⟩ := exists_scale_loadNormalizedToTopology Eseed
  let ground := scalePattern c (worldlinePattern gapOneTwoPhaseMode)
  let χ := scalePattern 2 ground
  have Eground : Q3ClosedPatternEvidence ground :=
    scalePattern_q3ClosedEvidence c hc Eseed
  have Eχ : Q3ClosedPatternEvidence χ :=
    scalePattern_q3ClosedEvidence 2 (by norm_num) Eground
  have hcert : CarrierCertificateEq ground χ := by
    simpa [χ] using carrierCertificateEq_scalePattern (by norm_num : (0 : ℝ) < 2) ground
  have hχ : LoadNormalizedToTopology χ := (hG ground χ hcert).mp hground
  have hratio : loadTopologyRatio χ = 4 := by
    have hratio0 : loadTopologyRatio ground = 1 :=
      (loadTopologyRatio_eq_one_iff_loadNormalizedToTopology ground).2 hground
    calc
      loadTopologyRatio χ = (2 : ℝ) ^ 2 * loadTopologyRatio ground := by
        simpa [χ] using loadTopologyRatio_scalePattern 2 ground
      _ = 4 := by rw [hratio0]; norm_num
  have hone : loadTopologyRatio χ = 1 :=
    (loadTopologyRatio_eq_one_iff_loadNormalizedToTopology χ).2 hχ
  exact (by norm_num : (4 : ℝ) ≠ 1) (hratio.symm.trans hone)
THEOREM loadNormalizedToTopology_not_carrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
loadNormalizedToTopology_not_carrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:283 
/-- `LoadNormalizedToTopology` is outside the class: the ground state and its
double share a carrier certificate (both are Q3 carriers with the same support
and topology) but disagree on the target. -/
theorem loadNormalizedToTopology_not_carrierCertificateGenesis :
    ¬ IsCarrierCertificateGenesisCondition LoadNormalizedToTopology := by
  intro hG
  obtain ⟨Eseed⟩ := q3MatterCarrier_worldlinePattern_gapOne
  obtain ⟨c, hc, hground⟩ := exists_scale_loadNormalizedToTopology Eseed
  let ground := scalePattern c (worldlinePattern gapOneTwoPhaseMode)
  let χ := scalePattern 2 ground
  have Eground : Q3ClosedPatternEvidence ground :=
    scalePattern_q3ClosedEvidence c hc Eseed
  have Eχ : Q3ClosedPatternEvidence χ :=
    scalePattern_q3ClosedEvidence 2 (by norm_num) Eground
  have hcert : CarrierCertificateEq ground χ := by
    simpa [χ] using carrierCertificateEq_scalePattern (by norm_num : (0 : ℝ) < 2) ground
  have hχ : LoadNormalizedToTopology χ := (hG ground χ hcert).mp hground
  have hratio : loadTopologyRatio χ = 4 := by
    have hratio0 : loadTopologyRatio ground = 1 :=
      (loadTopologyRatio_eq_one_iff_loadNormalizedToTopology ground).2 hground
    calc
      loadTopologyRatio χ = (2 : ℝ) ^ 2 * loadTopologyRatio ground := by
        simpa [χ] using loadTopologyRatio_scalePattern 2 ground
      _ = 4 := by rw [hratio0]; norm_num
  have hone : loadTopologyRatio χ = 1 :=
    (loadTopologyRatio_eq_one_iff_loadNormalizedToTopology χ).2 hχ
  exact (by norm_num : (4 : ℝ) ≠ 1) (hratio.symm.trans hone)
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 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]

What this page does not claim

The theorem does not claim that mass genesis is impossible in the framework. The theorem does not claim that rescaling is a gauge symmetry for all observables. The theorem does not claim that LoadNormalizedToTopology is the only route to mass ratios.

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