Masses Mass Genesis T10 Orbit Section No Go Scale Blind Fragment Does Not Entail

The scale-blind limit

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition event assigns a cost to a pattern. The framework's library, a machine-checked collection of formal theorems, proves a structural limit on any rule that tries to pick out the ground state, the pattern of lowest cost, using only shape and not size. The theorem scaleBlindFragment_does_not_entail_loadRecognitionCost_zero states that no predicate on patterns that is merely closed under positive rescaling can be a realization predicate satisfying R4, the ground-state selection law, as soon as it accepts one Q3 carrier. In plain language: a rule that cannot tell the difference between a pattern and a scaled copy of it can never force the cost to be zero, which is the condition for a settled state.

The proof is a doubling counterexample. Take any accepted carrier, rescale it onto its orbit zero, then double it. The result is still accepted by the scale-blind rule, but its load topology ratio is four. The cost function J(x) = (x + 1/x)/2 - 1 is zero only at x = 1, so a ratio of four gives a nonzero cost. The scale-blind rule accepts a pattern that the cost function says is not settled, so the rule cannot be a ground-state selector. The argument uses only the rescaling-closed property and the existence of one accepted carrier; it does not use the specific form of the cost or the ledger structure. This is what makes the result structural rather than a fact about one particular cost.

The theorem is a no-go result about a fragment, not about the whole foundation. The foundation is not scale-blind. The library exhibits a derived, load-side predicate, ledger occupancy, which is two-valued and therefore not closed under rescaling, and this predicate forces the settled amplitude to exactly one via settledAnchor_boolean_forces_unitAmplitude. An independence claim quantified over the whole foundation would be false. The scope is precise: the theorem rules out scale-blind rules, and it does not rule out rules that see scale.

The result matters because it draws a line. Any proposed law that ignores scale cannot be a ground-state selector, so the framework's own ground-state law must be scale-sensitive. The theorem also carries receipts that its hypotheses are load-bearing. A constraint with the same zero set as the cost but without the carrier condition can fail R4, and the empty predicate, which is rescaling-closed, does satisfy R4 vacuously. Both hypotheses, the accepted carrier and the same-zero-set condition, are needed. The theorem is proved in the machine-checked library with no sorry and no new axioms.

/-- **No-go 2, cost form.** No rescaling-closed predicate that accepts a Q3
carrier entails that the load recognition cost vanishes on everything it
accepts. -/
theorem scaleBlindFragment_does_not_entail_loadRecognitionCost_zero
    (P : LightPattern (Fin 8) → Prop)
    (hP : IsRescalingClosedPatternPredicate P)
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hacc : P ψ) :
    ¬ ∀ χ : LightPattern (Fin 8), P χ → loadRecognitionCost χ = 0 := by
  intro hall
  obtain ⟨χ, hPχ, _hcar, hratio⟩ :=
    rescalingClosedPredicate_accepts_ratioFour_carrier P hP E hacc
  exact
    loadRecognitionCost_ne_zero_of_loadTopologyRatio_four hratio (hall χ hPχ)

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

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

The theorem does not claim that the whole foundation is scale-blind or that an independence result holds over the full foundation. The theorem does not claim that every rescaling-closed predicate fails to be a ground-state selector; the empty predicate is a counterexample. The theorem does not claim that the cost function J is the only possible cost function.

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: