Encyclopedia Masses Masses Mass Genesis T10 Genesis Display Closure R4 Genesis Discharges Amplitude

ARTICLE 6 claims 6 theorems

Masses Mass Genesis T10 Genesis Display Closure R4 Genesis Discharges Amplitude

A single assumption about how matter appears closes a long-standing gap in the framework's mass theory, but the assumption itself remains a choice, not a derivation.

Verify this page

The genesis discharge

The declaration r4_genesis_discharges_amplitude_residual is the framework's answer to a specific open problem: why does a settled emission appear at the amplitude its topology predicts? The framework models a ledger, a discrete record of recognition events, being displayed into the continuum as a physical emission. The declaration proves that if one adopts a foundational law called R4, then every such settled emission posts at its predicted amplitude. The law R4 states that each realized pattern is the cost ground state of its scale orbit, meaning it sits at the minimum of a forced cost function. The proof is a theorem in the framework's machine-checked library of formal theorems, conditional on R4.

The physical reading is direct: creation displays every settled emission at the scale its topology predicts. This is the genesis condition that a conserved-ratio wall had said must exist. Selection cannot come from the flow of recognition events, so it enters at the act of creation, which here is the display of a ledger run into the continuum. The declaration is not a free lunch. It proves the organ is exactly R4 on the emission class, in both directions. Adopting the organ is adopting R4; nothing weaker is derived, and nothing here claims a derivation of R4 itself.

The law has constructible content. The framework constructs a doubled emission carrier, the same ledger run with doubled display amplitude and doubled pattern. This doubled carrier is a member of the emission realization class, yet it fails the residual: its amplitude is not its topology factor. Any realization class containing this doubled intended pattern violates R4, because the double sits at a load-to-topology ratio of four, where the recognition cost is nonzero, but R4 forces every realized carrier to cost zero. The law therefore excludes a constructed object, not a hypothetical one. The law is satisfiable: a factor-posting class satisfies R4, and the intended gap-one witness posts at factor with cost zero.

The declaration's role in the larger campaign is to fire the closure. Under R4, every settled emission carries the mass law, the absolute size law, and sigma zero, all derived inside the proof with no residual hypothesis supplied. Deleting the law restores the wall: without R4, a settled emission read exists whose amplitude is not the topology factor, and the residual stands. The dependence of the closure on the law is therefore a theorem rather than prose. The framework's own tags are explicit: the implications and equivalences proved here are THEOREMs, but every physical conclusion drawn under R4 is MODEL, because its weakest link is R4, a foundational model assertion. T10 bare remains open exactly at R4.

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_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 factorPostingClass_satisfies_r4 · intended_gapOne_carrier_posts_at_factor · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean
factorPostingClass_satisfies_r4 · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean:216 
/-- **M4a: the factor-posting class satisfies R4.** If a realization class
consists of settled Q3 anchors posting at their topology factor, every member
is cost-zero, hence orbit-minimal. -/
theorem factorPostingClass_satisfies_r4 :
    RecognitionGroundStateSelection
      (fun ψ : LightPattern (Fin 8) =>
        ∃ (a : ℝ) (_ : 0 < a),
          SettledAnchorWindow a ψ ∧ Q3MatterCarrier ψ ∧
            a = primitivePositiveStationaryFactorAmplitude ψ) := by
  intro ψ hreal c hc
  obtain ⟨a, ha, hwin, hcarrier, hfactor⟩ := hreal
  obtain ⟨E⟩ := hcarrier
  have hcost0 : loadRecognitionCost ψ = 0 :=
    (settledAnchor_loadRecognitionCost_zero_iff_amplitude E hwin
      (le_of_lt ha)).2 hfactor
  have hnorm : LoadNormalizedToTopology ψ :=
    (loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology E).1 hcost0
  exact intended_witness_satisfies_groundStateSelection_locally ψ hnorm c hc
intended_gapOne_carrier_posts_at_factor · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean:235 
/-- **M4b: the intended gap-one witness posts at factor with cost zero.** The
law accepts the intended physics. -/
theorem intended_gapOne_carrier_posts_at_factor
    (octave : Q3SettledLedgerOctave) :
    (EmittedForcedMatterInterfaceScaled.ofGapOneFactorAmplitude
      octave).readout.amplitude =
        primitivePositiveStationaryFactorAmplitude
          (EmittedForcedMatterInterfaceScaled.ofGapOneFactorAmplitude
            octave).readout.pattern ∧
      loadRecognitionCost (EmittedForcedMatterInterfaceScaled.ofGapOneFactorAmplitude
        octave).readout.pattern = 0 :=
  ⟨(EmittedForcedMatterInterfaceScaled.ofGapOneFactorAmplitude
      octave).amplitude_matches_factor,
   (EmittedForcedMatterInterfaceScaled.ofGapOneFactorAmplitude
      octave).pattern_sigma_zero⟩
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

The declaration does not prove R4 itself; it proves a conditional statement that assumes R4. The declaration does not derive the amplitude law from the five plain cost conditions alone. The declaration does not establish that the R4 model is physically true, only that it is consistent and constructible within the framework.

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