Encyclopedia Masses Masses Mass Genesis T10 Genesis Display Closure R4 Emission Iff Every Emission P

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Genesis Display Closure R4 Emission Iff Every Emission P

A machine-checked theorem ties the creation of matter to a single rule about scale, but the rule itself remains a chosen model.

Verify this page

The genesis condition

The declaration r4_emission_iff_every_emission_posts_at_factor is a formal equivalence inside the Recognition Science library. It states that a foundational law called R4 holds for a certain class of patterns if and only if every settled emission in that class displays at the amplitude its topology predicts. In plain terms: the rule that selects the ground state of a scale orbit is exactly the rule that creation shows each emission at its predicted size. The theorem proves these two statements are the same requirement, in both directions.

The background is a campaign to derive particle masses. The framework's library had already proved that once an emission posts at its topology factor amplitude, the mass law, absolute size, and zero recognition cost follow. The missing piece was what forces that posting. R4, adopted as a foundational model on 2024-07-24, supplies it: each realized pattern is the cost ground state of its scale orbit. The theorem here shows that adopting R4 on the emission class is not weaker and not stronger than demanding every emission post at its predicted scale. They are interchangeable.

The theorem also gives the law constructive content. The library constructs a doubled emission, the same ledger run displayed at twice the amplitude. That doubled object is a member of the emission realization class, yet it fails the posting condition and violates R4. So the law excludes a concrete, built object, not a hypothetical. The law is also satisfiable: a class where every member posts at its topology factor satisfies R4, and the intended gap-one witness posts at factor with zero cost.

In Recognition Science, this is the genesis condition: creation displays every settled emission at the scale its topology predicts. The conserved-ratio wall had said selection cannot come from the flow, so it must enter at the act of creation. This theorem names that entry point and closes the assembly relative to R4. Deleting R4 restores the wall, as a separate theorem shows.

What the theorem does not claim is equally precise. It does not derive R4 from anything more basic; R4 remains a foundational model assertion, the weakest link in every conclusion drawn under it. The implications and equivalences proved here are theorems, but the physical reading under hR4 is a model. T10 bare closure remains open exactly at R4.

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 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 doubledCarrier · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean
doubledCarrier · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean:116 
/-- The doubled emission carrier: same ledger run, doubled display amplitude,
doubled pattern. The emission world's envelope contains the off-scale double;
`reads_emitted` transports because the emitted window is linear in the
amplitude. -/
def doubledCarrier (c : EmittedScaledSettledReadoutCarrier) :
    EmittedScaledSettledReadoutCarrier where
  octave := c.octave
  amplitude := 2 * c.amplitude
  amplitude_pos := mul_pos (by norm_num) c.amplitude_pos
  pattern := scalePattern 2 c.pattern
  q3_carrier := scalePattern_q3MatterCarrier 2 (by norm_num) c.q3_carrier
  reads_emitted := by
    show (scalePattern 2 c.pattern).window 0 =
      (originEmittedPhotonStateScaled c.octave (2 * c.amplitude) _).window
    rw [originEmittedScaled_window_eq_scaledGapOne]
    have hread : c.pattern.window 0 =
        fun t => (c.amplitude : ℂ) * gapOneTwoPhaseMode t := by
      rw [← originEmittedScaled_window_eq_scaledGapOne
        c.octave c.amplitude c.amplitude_pos]
      exact c.reads_emitted
    funext t
    show (2 : ℂ) * c.pattern.window 0 t = _
    rw [hread]
    push_cast
    ring
THEOREM doubledCarrier_realized · doubled_intended_carrier_residual_fails · doubled_intended_carrier_violates_r4 · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean
doubledCarrier_realized · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean:142 
/-- The doubled carrier is a member of the emission realization class. -/
theorem doubledCarrier_realized (c : EmittedScaledSettledReadoutCarrier) :
    EmittedReadoutRealized (doubledCarrier c).pattern :=
  (doubledCarrier c).pattern_realized
doubled_intended_carrier_residual_fails · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean:147 
/-- **M3a: the doubled intended witness fails the residual.** The intended
gap-one interface posts at `factorAmp`; its double posts at `2 * factorAmp`,
and the factor amplitude is scale-invariant, so the double does not post at
its topology factor. -/
theorem doubled_intended_carrier_residual_fails
    (octave : Q3SettledLedgerOctave) :
    (doubledCarrier (EmittedForcedMatterInterfaceScaled.ofGapOneFactorAmplitude
      octave).readout).amplitude ≠
      primitivePositiveStationaryFactorAmplitude
        (doubledCarrier (EmittedForcedMatterInterfaceScaled.ofGapOneFactorAmplitude
          octave).readout).pattern := by
  intro heq
  set iface := EmittedForcedMatterInterfaceScaled.ofGapOneFactorAmplitude octave
  have hfactor_pos : 0 < primitivePositiveStationaryFactorAmplitude
      iface.readout.pattern := by
    have h := iface.amplitude_matches_factor
    rw [← h]
    exact iface.readout.amplitude_pos
  have hamp : (doubledCarrier iface.readout).amplitude =
      2 * iface.readout.amplitude := rfl
  have hfactor_scale :
      primitivePositiveStationaryFactorAmplitude
          (doubledCarrier iface.readout).pattern =
        primitivePositiveStationaryFactorAmplitude iface.readout.pattern :=
    primitivePositiveStationaryFactorAmplitude_scalePattern 2
      iface.readout.pattern
  rw [hamp, hfactor_scale, iface.amplitude_matches_factor] at heq
  have hzero : primitivePositiveStationaryFactorAmplitude
      iface.readout.pattern = 0 := by linarith
  exact (ne_of_gt hfactor_pos) hzero
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 r4_deleted_restores_residual_wall · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean
r4_deleted_restores_residual_wall · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean:278 
/-- **Deleting the law restores the wall.** Without R4, a settled emission
read exists whose amplitude is not the topology factor: the residual stands.
This is the campaign wall, re-exported so the dependence of the closure on the
law is a theorem rather than prose. -/
theorem r4_deleted_restores_residual_wall : ¬ PostedAmplitudeMatchesTopologyFactor :=
  postedAmplitudeMatchesTopologyFactor_wall

What this page does not claim

This answer does not claim R4 is derived from anything more basic; it remains a foundational model. This answer does not claim the physical reading under R4 is a theorem; it is a model. This answer does not claim T10 bare closure is complete; it is 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