Masses Mass Genesis T10 Orbit Section No Go Scale Blind Invariant Fragment Not R

The scale-blind limit

In the Recognition Science account, a recognition event is a discrete record in a ledger, and the framework's central cost function J(x) = (x + 1/x)/2 - 1 assigns a price to any pattern. The ground state of a system is the pattern that minimizes this cost, which the framework proves is equivalent to the cost being zero. A natural question is whether a simpler rule, one that only cares about a pattern's shape and not its overall scale, could also pick out the ground state. The declaration scaleBlindInvariantFragment_not_recognitionGroundStateSelection answers this in the negative: no predicate on patterns that is merely closed under positive rescaling can be a realization predicate satisfying the ground-state condition, as soon as it accepts one carrier pattern.

The proof is a doubling counterexample. Suppose such a rescaling-closed predicate accepts some pattern. Rescale that pattern onto its orbit's zero-cost point, then double it. The result is still accepted, because the predicate is scale-blind, yet its load topology ratio is four, where the cost function is provably nonzero. The accepted pattern therefore cannot be a ground state. This is a theorem in the framework's machine-checked library of formal theorems, with no unproved assumptions.

The scope is precise. The result applies only to the rescaling-closed fragment, and it is not an independence result about the whole foundation. The foundation is not scale-blind: a derived, load-side predicate called ledger occupancy is two-valued, so a settlement anchor window is Boolean, and this predicate forces the settled amplitude to exactly one. An independence claim quantified over the entire foundation would be false, and was refuted on 2026-07-27. The theorem also carries a witness showing the accepted-carrier hypothesis cannot be dropped: the empty predicate is rescaling-closed and does satisfy the ground-state condition vacuously.

What this changes is the search space. Any proposed law that is invariant under all positive rescalings cannot, on its own, be the law that selects the ground state. The framework's own load-side predicate, which is not scale-blind, is what does the selecting. The theorem does not claim that scale-blind rules are useless, only that they are insufficient for this one task.

/-- Same statement against full scale blindness. -/
theorem scaleBlindInvariantFragment_not_recognitionGroundStateSelection
    (Realized : LightPattern (Fin 8) → Prop)
    (hP : IsScaleBlindPatternPredicate Realized)
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hacc : Realized ψ) :
    ¬ RecognitionGroundStateSelection Realized :=
  scaleBlindFragment_not_recognitionGroundStateSelection Realized
    hP.rescalingClosed E hacc

/-- The doubling counterexample. A rescaling-closed predicate that accepts one
Q3 carrier also accepts a Q3 carrier sitting at load-to-topology ratio four. -/
theorem rescalingClosedPredicate_accepts_ratioFour_carrier
    (P : LightPattern (Fin 8) → Prop)
    (hP : IsRescalingClosedPatternPredicate P)
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hacc : P ψ) :
    ∃ χ : LightPattern (Fin 8),
      P χ ∧ Q3MatterCarrier χ ∧ loadTopologyRatio χ = 4 := by
  obtain ⟨c, hc, Ed, hratio⟩ := exists_doubled_ratio_four_of_q3ClosedEvidence E
  exact
    ⟨scalePattern 2 (scalePattern c ψ),
      hP 2 (by norm_num) _ (hP c hc ψ hacc), ⟨Ed⟩, hratio⟩

private theorem loadRecognitionCost_ne_zero_of_loadTopologyRatio_four
    {χ : LightPattern (Fin 8)} (h : loadTopologyRatio χ = 4) :
    loadRecognitionCost χ ≠ 0 := by
  intro hzero
  have hJ : Jcost (4 : ℝ) = 0 := by
    unfold loadRecognitionCost at hzero
    rwa [h] at hzero
  have h1 : (4 : ℝ) = 1 := (Jcost_eq_zero_iff (4 : ℝ) (by norm_num)).1 hJ
  norm_num at h1

/-- **The scope statement for no-go 2.** There is a derived, load-side predicate
of the present foundation which is outside the rescaling-closed fragment *and*
which fixes an absolute amplitude: a settled anchor whose window is Boolean has
posting amplitude exactly one.

So the foundation is not silent about the normalization and no-go 2 must never
be reported as independence from it. The honest reading is narrower and still
useful: nothing inside the scale-blind fragment can supply the missing sentence,
so a derivation has to come from the part of the foundation this predicate
inhabits. -/
theorem booleanOccupancy_is_derived_and_not_scaleBlind :
    ¬ IsRescalingClosedPatternPredicate BooleanSettledAnchorWindow ∧
      ∀ (a : ℝ) (χ : LightPattern (Fin 8)),
        SettledAnchorWindow a χ → BooleanSettledAnchorWindow χ → 0 < a →
          a = 1 :=
  ⟨booleanSettledAnchorWindow_not_rescalingClosed,
    fun _a _χ hwin hbool ha =>
      settledAnchor_boolean_forces_unitAmplitude hwin hbool ha⟩

/-- Deleting the accepted-carrier hypothesis from no-go 2 makes it false. The
empty realization predicate is rescaling-closed and satisfies R4 vacuously, so
the no-go bites exactly on predicates that accept some matter. -/
theorem acceptedCarrier_hypothesis_is_load_bearing :
    IsRescalingClosedPatternPredicate (fun _ => False) ∧
      RecognitionGroundStateSelection (fun _ => False) :=
  ⟨fun _ _ _ h => h.elim, fun _ h => h.elim⟩

What this page does not claim

This theorem does not claim that scale-blind rules are useless in general, only that they cannot select the ground state. This theorem does not claim an independence result about the whole foundation; the foundation itself is not scale-blind. This theorem does not claim that the empty predicate is a physically meaningful realization predicate; it is only a logical witness.

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