Encyclopedia Masses Masses Mass Genesis R4 Genesis Route Cdscratch Q3 Matter Carrier Does Not Force

ARTICLE 4 claims 4 theorems

Masses Mass Genesis R4 Genesis Route Cdscratch Q3 Matter Carrier Does Not Force

A machine-checked theorem shows that any creation rule based only on a particle's structural certificate must admit a doubled version with four times the mass, so no such rule can single out the normalized state.

Verify this page

A limit on genesis rules

In the Recognition Science framework, a stable particle pattern is admitted by a creation rule, a condition that decides whether a given pattern is a valid matter carrier. The framework's machine-checked library of formal theorems has proved a limit on what such rules can do. The theorem q3MatterCarrier_does_not_force_loadNormalized_of_certificate establishes that no creation rule which depends only on a pattern's carrier certificate can force the pattern to have a specific normalized load-to-topology ratio. In plain terms, if a rule accepts a particle, it must also accept a version of that particle that has been rescaled by a factor of two, and that doubled version has a different, four-times-larger mass ratio.

The carrier certificate is the discrete and relational data the library actually uses to admit patterns: the pattern's 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. A genesis condition is defined as one that gives the same verdict for any two patterns sharing this certificate. The theorem proves that any such condition, if it accepts any Q3 matter carrier at all, also accepts a Q3 carrier whose load-to-topology ratio is four. Since the normalized target requires a ratio of one, no certificate-based rule can force it. The result is not vacuous: the class of certificate-based rules is properly inhabited by Q3MatterCarrier itself, which does real work, while the target predicate LoadNormalizedToTopology is shown to fall outside the class.

The theorem is a no-go result, a proof that a certain hoped-for derivation is impossible. It does not claim that mass normalization is false or unattainable, only that it cannot be forced by the class of creation-side conditions defined by certificate agreement. The proof relies on the fact that rescaling a pattern by a positive factor preserves the carrier certificate, a fact that is proved as a corollary, not assumed. The result also does not extend to well-formedness predicates that tie topology to the window, to golden-ring or integrality routes, or to Boolean-occupancy amplitude pins, all of which lie outside the class it covers.

What the theorem changes is the search space. Anyone hoping to derive the normalized load-to-topology ratio from creation-side conditions must look beyond the carrier certificate, to conditions that read absolute window magnitudes or other data not preserved by rescaling. The certificate alone cannot do the job, and the framework now knows that with certainty.

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 carrierCertificateGenesis_accepts_ratioFour · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
carrierCertificateGenesis_accepts_ratioFour · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:220 
/-- If a carrier-certificate genesis condition accepts any Q3 carrier, it also
accepts a Q3 carrier at load-to-topology ratio four. -/
theorem carrierCertificateGenesis_accepts_ratioFour
    (G : LightPattern (Fin 8) → Prop)
    (hG : IsCarrierCertificateGenesisCondition G)
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hacc : G ψ) :
    ∃ χ : LightPattern (Fin 8),
      G χ ∧ Q3MatterCarrier χ ∧ loadTopologyRatio χ = 4 := by
  obtain ⟨c, hc, Ed, hratio⟩ := exists_doubled_ratio_four_of_q3ClosedEvidence E
  let χ := scalePattern 2 (scalePattern c ψ)
  have h1 : G (scalePattern c ψ) :=
    (carrierCertificateGenesis_scaleInvariant G hG hc ψ).mp hacc
  have h2 : G χ :=
    (carrierCertificateGenesis_scaleInvariant G hG (by norm_num : (0 : ℝ) < 2)
      (scalePattern c ψ)).mp h1
  exact ⟨χ, h2, ⟨Ed⟩, hratio⟩
THEOREM q3MatterCarrier_isCarrierCertificateGenesis · loadNormalizedToTopology_not_carrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean
q3MatterCarrier_isCarrierCertificateGenesis · IndisputableMonolith/Masses/MassGenesis/R4GenesisRouteCDScratch.lean:257 
/-- Concrete instance: `Q3MatterCarrier` itself cannot force the target. -/
theorem q3MatterCarrier_isCarrierCertificateGenesis :
    IsCarrierCertificateGenesisCondition Q3MatterCarrier := by
  intro ψ χ h
  constructor
  · intro ⟨E⟩
    refine ⟨⟨?_, ?_, ?_⟩⟩
    · exact h.2.2.1.mp E.stable
    · exact h.2.2.2.1.mp E.full_support
    · exact h.2.2.2.2.mp E.window_equivariant
  · intro ⟨E⟩
    refine ⟨⟨?_, ?_, ?_⟩⟩
    · exact h.2.2.1.mpr E.stable
    · exact h.2.2.2.1.mpr E.full_support
    · exact h.2.2.2.2.mpr E.window_equivariant
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 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

What this page does not claim

The theorem does not claim that mass normalization is false or unattainable, only that certificate-based rules cannot force it. It does not claim that all creation rules fail to force the target, only those defined by carrier certificate agreement. It does not cover well-formedness predicates, golden-ring routes, or Boolean-occupancy amplitude pins outside the class.

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