Encyclopedia Masses Masses Mass Genesis T10 Genesis Display Closure Doubled Intended Carrier Residua

ARTICLE 3 claims 2 theorems 1 model

Masses Mass Genesis T10 Genesis Display Closure Doubled Intended Carrier Residua

A formal proof shows that a specific, constructed counterexample fails a proposed law of nature, demonstrating the law has real content.

Verify this page

The doubled emission test

In the Recognition Science framework, a ledger is a discrete record of events. The framework models the universe as maintaining such a record, and a "recognition" is a single entry in that record. A central question is how these discrete records, or "ledger runs," are displayed into the continuous world we observe. The specific declaration `doubled_intended_carrier_residual_fails` is a formal statement, checked by a machine, that establishes a precise fact about this display process.

The declaration concerns a particular kind of display, called a "settled emission readout carrier." This is a ledger run that is read out at a certain positive amplitude, or strength. The framework proposes a law, called R4, which states that each realized pattern must be the cost ground state of its scale orbit. In plainer terms, this law says that when a ledger run is displayed, its amplitude must match a specific value predicted by its topology, or structure. The declaration in question tests this law by constructing a specific counterexample: it takes a particular, intended carrier and doubles its display amplitude, creating a new carrier that is twice as strong.

The declaration `doubled_intended_carrier_residual_fails` proves that this doubled carrier does not post at its topology factor amplitude. In other words, the doubled emission fails to satisfy the proposed law. This is a constructive result: it shows the law R4 is not a trivial or empty statement. It has the power to exclude a specific, built object. A companion declaration, `doubled_intended_carrier_violates_r4`, goes further and proves that any realization class containing this doubled pattern would violate R4. This establishes that the law has real, exclusionary content.

However, the declaration does not claim that R4 itself is true. The declarations are implications: they show that if R4 holds, then certain consequences follow. The law R4 is a foundational model assertion, a chosen premise, not a derived statement. The framework's own documentation is explicit on this point: adopting the organ that discharges the residual is adopting R4; nothing weaker is derived, and nothing here claims a derivation of R4. The declaration also does not claim that the doubled carrier is a physically real object. It is a constructed mathematical object, used to test the consistency of the proposed law. The framework also proves the law is satisfiable: the intended, non-doubled carrier does post at its factor with zero cost, showing the law accepts the intended physics.

The practical consequence is that the framework has a rigorous, machine-checked demonstration that its proposed law of creation has teeth. It is not a vacuous principle; it excludes a specific, constructed possibility. This is a step toward closing a long-standing gap in the framework's derivation of particle masses, but it is a closure relative to a chosen law, not an absolute proof.

THEOREM doubled_intended_carrier_residual_fails · IndisputableMonolith/Masses/MassGenesis/T10GenesisDisplayClosure.lean
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
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
MODEL factorPostingClass_satisfies_r4 · 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

What this page does not claim

The declaration does not prove the law R4 is true; it only proves consequences that follow if R4 is assumed. The doubled carrier is a constructed mathematical object, not a claim about a physically real emission. This result does not close the T10 gap absolutely; it closes it only relative to the chosen foundational law 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