Masses Mass Genesis T10 Recognition Ground State Selection

The ground-state selection

The mass law in Recognition Science reduces to a single variational sentence. A realized pattern is the recognition-cost ground state of its scale orbit: every positive rescaling of it costs at least as much to recognize. In plainer words, the version of a pattern that nature actually realizes is the cheapest version of itself under rescaling. The framework models this with the principle recognition ground-state selection, which says that a realized pattern is the one with the lowest recognition cost, the price the universe pays to register a pattern.

The principle is an adopted assertion, not a theorem. The framework's library of formal theorems records it as a foundational model, in the same series as earlier structural assumptions. The critical fact is that this principle is logically equivalent, pointwise, to the premise the campaign had forbidden itself from using as an input: that the recognition load of a realized pattern is zero. The machine-checked equivalence theorem states this directly. Adopting the principle is asserting in general form the very thing the mass-genesis campaign set out to derive.

What the campaign did establish is that the mass law reduces to exactly this one sentence. Every other mechanism in it is derived: the coherence quantum forced by channel-block self-similarity, the binary sector factor from cube geometry, and the phi-ladder transport. The sentence itself cannot come from the dynamics, because the conserved-ratio wall shows the load-to-topology ratio is a constant of the motion. Any future derivation of this principle has to come from genesis, the framework's term for the origin of the ledger itself.

The principle is not vacuous. The intended witness, a load-normalized pattern with ratio one, satisfies the inequality against every rescaling. The doubled witness, with ratio four, is rejected: rescaling by one half reaches cost zero, while the witness itself has nonzero cost. This discrimination pair shows the principle accepts the intended physics and rejects a decoy. Without the principle, the campaign's residual remains false; deleting it restores the wall.

In the framework, this is why matter is what costs nothing to recognize. The physical reading is that a realized pattern is the cheapest version of itself under rescaling, so matter is what costs nothing to recognize. That is why the sentence is a natural one to adopt rather than an arbitrary patch. The consequences drawn through it, such as load normalization and the amplitude equation, are implications in the library, but every physical conclusion is a model, because its weakest link is an adopted assertion.

/-- **Honest core.** On a Q3 carrier, the R4 inequality at `ψ` is logically
equivalent to `loadRecognitionCost ψ = 0`. Forward: zero cost is a global
minimum of `Jcost` on the positive reals, so it is at most the cost of any
rescaling. Backward: the scale orbit contains a representative of cost zero
(`exists_scale_loadNormalizedToTopology`), so the inequality forces cost
`≤ 0`, and nonnegativity gives equality. -/
theorem groundStateSelection_pointwise_iff_loadRecognitionCost_zero
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ) :
    (∀ c : ℝ, 0 < c →
      loadRecognitionCost ψ ≤ loadRecognitionCost (scalePattern c ψ)) ↔
      loadRecognitionCost ψ = 0 := by
  constructor
  · intro hR4
    obtain ⟨c, hc, hground⟩ := exists_scale_loadNormalizedToTopology E
    have Escaled : Q3ClosedPatternEvidence (scalePattern c ψ) :=
      scalePattern_q3ClosedEvidence c hc E
    have hle : loadRecognitionCost ψ ≤
        loadRecognitionCost (scalePattern c ψ) :=
      hR4 c hc
    have hscaled0 : loadRecognitionCost (scalePattern c ψ) = 0 :=
      (loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology Escaled).2
        hground
    have hle0 : loadRecognitionCost ψ ≤ 0 := by
      rw [hscaled0] at hle
      exact hle
    have hnonneg : 0 ≤ loadRecognitionCost ψ :=
      loadRecognitionCost_nonneg_of_q3ClosedEvidence E
    exact le_antisymm hle0 hnonneg
  · intro hcost0 c hc
    have Escaled : Q3ClosedPatternEvidence (scalePattern c ψ) :=
      scalePattern_q3ClosedEvidence c hc E
    have hnonneg : 0 ≤ loadRecognitionCost (scalePattern c ψ) :=
      loadRecognitionCost_nonneg_of_q3ClosedEvidence Escaled
    rw [hcost0]
    exact hnonneg

/-- The concrete ratio-four witness of `exists_loadTopologyRatio_eq_four` is
rejected by R4: rescaling by one half reaches cost zero, while the witness
itself has cost `Jcost 4 ≠ 0` (since `4 ≠ 1`). No realization predicate that
accepts that witness can satisfy `RecognitionGroundStateSelection`. This is
decoy rejection, not a proof that R4 is weaker than cost-zero. -/
theorem doubled_witness_violates_groundStateSelection :
    ∃ ψ : LightPattern (Fin 8),
      loadTopologyRatio ψ = 4 ∧
        ∀ (Realized : LightPattern (Fin 8) → Prop),
          Realized ψ → ¬ RecognitionGroundStateSelection Realized := by
  obtain ⟨ψ, hratio, _hnot⟩ := exists_loadTopologyRatio_eq_four
  refine ⟨ψ, hratio, ?_⟩
  intro Realized hreal hR4
  have hle : loadRecognitionCost ψ ≤
      loadRecognitionCost (scalePattern (1 / 2 : ℝ) ψ) :=
    hR4 ψ hreal (1 / 2) (by norm_num)
  have hcostψ : loadRecognitionCost ψ = Jcost 4 := by
    unfold loadRecognitionCost
    rw [hratio]
  have hratio_scaled :
      loadTopologyRatio (scalePattern (1 / 2 : ℝ) ψ) = 1 := by
    calc
      loadTopologyRatio (scalePattern (1 / 2 : ℝ) ψ) =
          (1 / 2 : ℝ) ^ 2 * loadTopologyRatio ψ :=
        loadTopologyRatio_scalePattern (1 / 2) ψ
      _ = (1 / 4 : ℝ) * 4 := by
        rw [hratio]
        norm_num
      _ = 1 := by norm_num
  have hcost_scaled :
      loadRecognitionCost (scalePattern (1 / 2 : ℝ) ψ) = 0 := by
    unfold loadRecognitionCost
    rw [hratio_scaled, Jcost_unit0]
  have hle' : Jcost 4 ≤ 0 := by
    rw [hcostψ, hcost_scaled] at hle
    exact hle
  have hne : Jcost 4 ≠ 0 := by
    intro hzero
    have hone : (4 : ℝ) = 1 :=
      (Jcost_eq_zero_iff (4 : ℝ) (by norm_num)).1 hzero
    norm_num at hone
  have hnonneg : 0 ≤ Jcost 4 := Jcost_nonneg (by norm_num : (0 : ℝ) < 4)
  exact hne (le_antisymm hle' hnonneg)

/-- Without R4, the campaign residual remains false. Deleting the law restores
the wall. -/
theorem groundStateSelection_deleted_restores_wall :
    ¬ PostedAmplitudeMatchesTopologyFactor :=
  postedAmplitudeMatchesTopologyFactor_wall

What this page does not claim

This module does not derive the residual; it adopts it as a foundational model. The principle is not logically weaker than the zero-load premise; it is equivalent to it. No physical conclusion drawn through the principle is a theorem, because the weakest link is an adopted assertion.

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/T10RecognitionGroundStateSelection.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: