Masses Mass Genesis T10 Recognition Ground State Selection Ground State Selectio

The equivalence theorem

The theorem groundStateSelection_pointwise_iff_loadRecognitionCost_zero states a logical equivalence. In plain language: for any light pattern on an eight-tick carrier, the statement "every positive rescaling of this pattern costs at least as much to recognize as the pattern itself" is true if and only if the pattern's recognition cost is exactly zero. The recognition cost is a number the framework assigns to a pattern, measuring how expensive it is to identify that pattern against a ledger, a discrete record of events. The theorem is proved in the machine-checked library of formal theorems, with no unproved assumptions added.

The forward direction is direct: if a pattern costs zero to recognize, then zero is the smallest possible cost, so every rescaling costs at least zero. The backward direction uses a deeper fact: the scale orbit of a pattern contains a representative whose cost is zero, so if every rescaling costs at least as much as the original, the original's cost must be at most zero, and costs are never negative. The theorem therefore collapses two superficially different demands into one.

In Recognition Science, this equivalence is the logical core of a foundational model assertion called R4: a realized pattern is the recognition-cost ground state of its scale orbit, meaning matter is what costs nothing to recognize. The theorem proves that this assertion, restricted to one pattern, is exactly the premise the broader campaign had forbidden as an input. Adopting R4 in general form is therefore asserting the very thing the campaign set out to derive. The equivalence does not make the residual a derivation; it shows the assertion is not logically weaker than the cost-zero premise.

The theorem also powers two conditional results. Under R4, a realized Q3-closed pattern is load-normalized to topology, and a settled pattern posts at the topology-factor amplitude. Both are proved as implications from R4, but their physical conclusions are MODEL, because the weakest link is the adopted assertion, not a derived law. Without R4, the campaign residual remains false; deleting the law restores the wall.

What the theorem does not claim is as important as what it proves. It does not show that R4 is derivable from the dynamics; the conserved-ratio wall shows the load-to-topology ratio is a constant of the motion, so the sentence cannot come from the dynamics. It does not show that R4 is logically weaker than the cost-zero premise; the equivalence shows it is not. And it does not establish that any physical pattern actually satisfies the condition; that depends on the adopted assertion, which remains a foundational model choice, not a theorem.

/-- **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

/-- Under R4, a realized Q3-closed pattern is load-normalized to topology.
THEOREM as an implication; the physical conclusion is MODEL. -/
theorem groundStateSelection_forces_loadNormalized
    (Realized : LightPattern (Fin 8) → Prop)
    (hR4 : RecognitionGroundStateSelection Realized)
    {ψ : LightPattern (Fin 8)}
    (hreal : Realized ψ)
    (E : Q3ClosedPatternEvidence ψ) :
    LoadNormalizedToTopology ψ := by
  have hpointwise :
      ∀ c : ℝ, 0 < c →
        loadRecognitionCost ψ ≤ loadRecognitionCost (scalePattern c ψ) :=
    fun c hc => hR4 ψ hreal c hc
  have hcost0 : loadRecognitionCost ψ = 0 :=
    (groundStateSelection_pointwise_iff_loadRecognitionCost_zero E).1
      hpointwise
  exact (loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology E).1 hcost0

/-- Under R4, a realized settled Q3-closed pattern posts at the topology-factor
amplitude. THEOREM as an implication from R4; not a derivation of the residual
as bare physics. -/
theorem groundStateSelection_forces_amplitude
    (Realized : LightPattern (Fin 8) → Prop)
    (hR4 : RecognitionGroundStateSelection Realized)
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hreal : Realized ψ)
    (E : Q3ClosedPatternEvidence ψ)
    (hwin : SettledAnchorWindow a ψ)
    (ha : 0 ≤ a) :
    a = primitivePositiveStationaryFactorAmplitude ψ := by
  have hnorm : LoadNormalizedToTopology ψ :=
    groundStateSelection_forces_loadNormalized Realized hR4 hreal E
  have hcost0 : loadRecognitionCost ψ = 0 :=
    (loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology E).2 hnorm
  exact
    (settledAnchor_loadRecognitionCost_zero_iff_amplitude E hwin ha).1 hcost0

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

The theorem does not show that R4 is derivable from the dynamics; the conserved-ratio wall blocks that. The theorem does not show that R4 is logically weaker than the cost-zero premise; it shows the opposite. The theorem does not establish that any physical pattern satisfies the ground-state condition; that depends on the adopted foundational model.

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: