Encyclopedia Masses Masses Mass Genesis T10 Recognition Ground State Selection Doubled Witness Viola

ARTICLE 4 claims 3 theorems 1 model

Masses Mass Genesis T10 Recognition Ground State Selection Doubled Witness Viola

A formal test shows why a candidate pattern with twice the expected load fails the selection rule, while the intended pattern passes.

Verify this page

The doubled witness

In the Recognition Science framework, a realized pattern is one that nature actually uses. The framework models a selection rule for which patterns count as realized: a pattern is realized only if it is the cheapest version of itself under rescaling. Rescaling means stretching or shrinking the pattern's internal scale. The rule says that any positive rescaling must cost at least as much to recognize as the original pattern. This rule is called recognition ground-state selection, and it is an adopted model assertion, not a derived theorem.

The declaration doubled_witness_violates_groundStateSelection proves a precise fact about one specific pattern. That pattern has a load-to-topology ratio of four, meaning its recognition load is four times its topology factor. The theorem shows that this doubled witness is rejected: no realization predicate that accepts this pattern can satisfy the selection rule. The reason is concrete. Rescaling this pattern by one half reaches a recognition cost of zero, while the witness itself has a nonzero cost. Since the rule demands that every rescaling cost at least as much, the doubled witness fails.

The same module proves the intended pattern passes. A pattern that is load-normalized to its topology factor has recognition cost zero, and zero is a global minimum of the cost function on the positive reals. So every positive rescaling costs at least zero, and the rule accepts it. This pair, rejection of the doubled witness and acceptance of the intended one, shows the rule is not vacuous: it actually discriminates between candidate patterns.

The doubled-witness theorem is a THEOREM in the framework's machine-checked library of formal theorems. It states an implication about the selection rule. What it does not claim is that the selection rule itself is derived from anything deeper. The rule is an adopted assertion, recorded as a foundational model. The theorem also does not show that the rule is logically weaker than requiring zero recognition cost; in fact, on a Q3 carrier the rule is pointwise equivalent to that requirement. Without the adopted rule, the campaign's residual claim about amplitude remains false, and the wall against deriving it stands.

THEOREM doubled_witness_violates_groundStateSelection · IndisputableMonolith/Masses/MassGenesis/T10RecognitionGroundStateSelection.lean
doubled_witness_violates_groundStateSelection · IndisputableMonolith/Masses/MassGenesis/T10RecognitionGroundStateSelection.lean:156 
/-- 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)
THEOREM intended_witness_satisfies_groundStateSelection_locally · IndisputableMonolith/Masses/MassGenesis/T10RecognitionGroundStateSelection.lean
intended_witness_satisfies_groundStateSelection_locally · IndisputableMonolith/Masses/MassGenesis/T10RecognitionGroundStateSelection.lean:200 
/-- The intended (load-normalized, ratio-one) pattern has recognition cost
zero and therefore satisfies the R4 inequality against every positive
rescaling, via `Jcost_nonneg`. Non-vacuity: the law accepts the intended
physics. -/
theorem intended_witness_satisfies_groundStateSelection_locally
    (ψ : LightPattern (Fin 8))
    (hnorm : LoadNormalizedToTopology ψ)
    (c : ℝ) (hc : 0 < c) :
    loadRecognitionCost ψ ≤ loadRecognitionCost (scalePattern c ψ) := by
  have hr : loadTopologyRatio ψ = 1 :=
    (loadTopologyRatio_eq_one_iff_loadNormalizedToTopology ψ).2 hnorm
  have hcost0 : loadRecognitionCost ψ = 0 := by
    unfold loadRecognitionCost
    rw [hr, Jcost_unit0]
  have hratio_scaled :
      loadTopologyRatio (scalePattern c ψ) = c ^ 2 := by
    rw [loadTopologyRatio_scalePattern c ψ, hr, mul_one]
  have hpos : 0 < loadTopologyRatio (scalePattern c ψ) := by
    rw [hratio_scaled]
    exact pow_pos hc 2
  have hnonneg : 0 ≤ loadRecognitionCost (scalePattern c ψ) := by
    unfold loadRecognitionCost
    exact Jcost_nonneg hpos
  rw [hcost0]
  exact hnonneg
MODEL RecognitionGroundStateSelection · IndisputableMonolith/Masses/MassGenesis/T10RecognitionGroundStateSelection.lean
RecognitionGroundStateSelection · IndisputableMonolith/Masses/MassGenesis/T10RecognitionGroundStateSelection.lean:63 
/-- **FOUNDATIONAL MODEL SCR R4.** A realized pattern is the recognition-cost
ground state of its scale orbit: every positive rescaling costs at least as
much. Parametric in `Realized` so the law stays target-blind.

On any Q3 carrier this is pointwise equivalent to
`loadRecognitionCost ψ = 0` (see
`groundStateSelection_pointwise_iff_loadRecognitionCost_zero`). -/
def RecognitionGroundStateSelection
    (Realized : LightPattern (Fin 8) → Prop) : Prop :=
  ∀ ψ : LightPattern (Fin 8), Realized ψ →
    ∀ c : ℝ, 0 < c →
      loadRecognitionCost ψ ≤ loadRecognitionCost (scalePattern c ψ)
THEOREM groundStateSelection_deleted_restores_wall · IndisputableMonolith/Masses/MassGenesis/T10RecognitionGroundStateSelection.lean
groundStateSelection_deleted_restores_wall · IndisputableMonolith/Masses/MassGenesis/T10RecognitionGroundStateSelection.lean:226 
/-- 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 selection rule is derived from dynamics or from any deeper principle. The doubled-witness theorem shows the rule is logically weaker than requiring zero recognition cost. The physical claim that matter is what costs nothing to recognize is a proven theorem.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND