Encyclopedia Masses Masses Mass Genesis T10 Genesis Display Closure

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Genesis Display Closure

A machine-checked library shows that if creation itself obeys one ground-state law, then every particle's mass, size, and stability follow with no further assumptions.

Verify this page

The genesis display closure

The ledger, a discrete record of recognition events, is the central object of Recognition Science. This work closes a long-standing gap in the framework's account of particle masses. The gap was a single unproved field: the claim that a settled emission posts at its topology factor amplitude. Everything downstream, the mass law, the absolute size law, and the zero-cost condition, was already proved from that field. The open question was what could discharge it.

The answer is that the missing field follows from the foundational law R4, which states that each realized pattern is the cost ground state of its scale orbit. Applied to the class of patterns that arise as ledger runs displayed into the continuum, R4 forces every settled emission to post at its topology factor. The physical reading is that creation displays every settled emission at the scale its topology predicts. This is the genesis condition the conserved-ratio wall said had to exist: selection cannot come from the flow, so it enters at the act of creation.

The result holds in both directions. R4 holds on the emission class if and only if every settled emission posts at its factor, so adopting the organ is exactly adopting R4. The law has constructible content: a doubled emission carrier is built, a same ledger run at doubled amplitude, and any realization class containing it violates R4. This shows the law excludes a real object, not a hypothetical one. The law is also satisfiable: the intended gap-one witness posts at factor with zero cost.

With the residual discharged, the closure fires. Under R4, every settled emission assembles into the forced-matter interface with no residual hypothesis supplied. The theorem genesis_closure_fires proves that rest mass equals predicted mass, amplitude squared equals predicted mass over sixteen, and the recognition cost is zero. Deleting the law restores the wall: without R4, a settled emission read exists whose amplitude is not the topology factor. The dependence of the closure on the law is therefore a theorem, not prose.

The honest accounting is precise. The implications and equivalences proved here are theorems in the machine-checked library. Every physical conclusion drawn under R4 is a model, because its weakest link is R4 itself, a foundational model assertion. This is closure relative to R4, not bare closure. Bare T10 remains open exactly at R4. No sorry and no new axioms appear in the work.

THEOREM r4_genesis_discharges_amplitude_residual · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean
r4_genesis_discharges_amplitude_residual · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean:78 
/-- **M1: R4 at genesis discharges the campaign residual.** Under R4 applied
to the emission realization class, every settled emission posts at the
topology factor amplitude. THEOREM as an implication from R4; the physical
conclusion is MODEL. -/
theorem r4_genesis_discharges_amplitude_residual
    (hR4 : RecognitionGroundStateSelection EmittedReadoutRealized)
    (c : EmittedScaledSettledReadoutCarrier) :
    c.amplitude = primitivePositiveStationaryFactorAmplitude c.pattern := by
  obtain ⟨E⟩ := c.q3_carrier
  exact groundStateSelection_forces_amplitude EmittedReadoutRealized hR4
    c.pattern_realized E c.settled_anchor (le_of_lt c.amplitude_pos)
THEOREM r4_emission_iff_every_emission_posts_at_factor · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean
r4_emission_iff_every_emission_posts_at_factor · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean:90 
/-- **M2: the organ is exactly R4 on the emission class.** R4 holds of the
ledger-image realization class if and only if every settled emission posts at
its topology factor scale. Forward is the residual discharge; backward is that
a factor-posting pattern is cost-zero on its settled anchor, hence
orbit-minimal. This is the honest accounting: adopting the organ is adopting
R4 here. -/
theorem r4_emission_iff_every_emission_posts_at_factor :
    RecognitionGroundStateSelection EmittedReadoutRealized ↔
      ∀ c : EmittedScaledSettledReadoutCarrier,
        c.amplitude = primitivePositiveStationaryFactorAmplitude c.pattern := by
  constructor
  · intro hR4 c
    exact r4_genesis_discharges_amplitude_residual hR4 c
  · intro hall ψ hreal c hc
    obtain ⟨car, rfl⟩ := hreal
    obtain ⟨E⟩ := car.q3_carrier
    have hcost0 : loadRecognitionCost car.pattern = 0 :=
      (settledAnchor_loadRecognitionCost_zero_iff_amplitude
        E car.settled_anchor (le_of_lt car.amplitude_pos)).2 (hall car)
    have hnorm : LoadNormalizedToTopology car.pattern :=
      (loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology E).1 hcost0
    exact intended_witness_satisfies_groundStateSelection_locally
      car.pattern hnorm c hc
THEOREM doubled_intended_carrier_violates_r4 · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean
doubled_intended_carrier_violates_r4 · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean:178 
/-- **M3b: any realization class containing the doubled intended pattern
violates R4.** The double sits at load-to-topology ratio four, where the
recognition cost is nonzero, but R4 forces every realized Q3 carrier to cost
zero. The law therefore excludes a constructed object. -/
theorem doubled_intended_carrier_violates_r4
    (octave : Q3SettledLedgerOctave)
    (Realized : LightPattern (Fin 8) → Prop)
    (hmem : Realized (doubledCarrier
      (EmittedForcedMatterInterfaceScaled.ofGapOneFactorAmplitude
        octave).readout).pattern) :
    ¬ RecognitionGroundStateSelection Realized := by
  intro hR4
  set iface := EmittedForcedMatterInterfaceScaled.ofGapOneFactorAmplitude octave
  have hpat : (doubledCarrier iface.readout).pattern =
      scalePattern 2 iface.readout.pattern := rfl
  obtain ⟨E⟩ := (doubledCarrier iface.readout).q3_carrier
  have hcost0 : loadRecognitionCost (doubledCarrier iface.readout).pattern = 0 := by
    have hnorm : LoadNormalizedToTopology (doubledCarrier iface.readout).pattern :=
      groundStateSelection_forces_loadNormalized Realized hR4 hmem E
    exact (loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology E).2 hnorm
  have hratio4 : loadTopologyRatio (doubledCarrier iface.readout).pattern = 4 := by
    have h1 : loadTopologyRatio iface.readout.pattern = 1 :=
      (loadTopologyRatio_eq_one_iff_loadNormalizedToTopology _).2
        iface.loadNormalized
    calc
      loadTopologyRatio (doubledCarrier iface.readout).pattern
          = (2 : ℝ) ^ 2 * loadTopologyRatio iface.readout.pattern := by
            rw [hpat]; exact loadTopologyRatio_scalePattern 2 iface.readout.pattern
      _ = 4 := by rw [h1]; norm_num
  have hJ : Jcost (4 : ℝ) = 0 := by
    have h := hcost0
    unfold loadRecognitionCost at h
    rwa [hratio4] at h
  have h1 : (4 : ℝ) = 1 := (Jcost_eq_zero_iff 4 (by norm_num)).1 hJ
  norm_num at h1
THEOREM genesis_closure_fires · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean
genesis_closure_fires · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean:264 
/-- **M5: the staged closure relative to R4.** Under R4, every settled
emission carries the mass law, the absolute size law, and sigma zero.
MODEL (weakest link R4). -/
theorem genesis_closure_fires
    (hR4 : RecognitionGroundStateSelection EmittedReadoutRealized)
    (c : EmittedScaledSettledReadoutCarrier) :
    restMass c.pattern = predictedMass c.pattern ∧
      c.amplitude ^ 2 = predictedMass c.pattern / 16 ∧
        loadRecognitionCost c.pattern = 0 :=
  let iface := EmittedForcedMatterInterfaceScaled.ofReadout_of_R4 hR4 c
  ⟨iface.restMass_eq_predictedMass,
   iface.amplitude_sq_eq_predictedMass_div_sixteen,
   iface.pattern_sigma_zero⟩

What this page does not claim

This module does not prove R4 itself; it proves closure relative to R4. No physical conclusion here is a theorem; all physical conclusions are models whose weakest link is R4. The module does not claim that bare T10 is closed; bare T10 remains open exactly at R4.

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/T10GenesisDisplayClosure.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