Encyclopedia Masses Masses Mass Genesis T10 Orbit Section No Go

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Orbit Section No Go

Two machine-checked theorems show that any constraint which only cares about a pattern's shape, not its size, cannot select the unique settled state the framework requires.

Verify this page

Two limits on the load

In the Recognition Science account, a ledger is a discrete record of events, and each possible event pattern carries a cost, a real number measuring how far the pattern sits from the settled state. The framework's core result forces a specific cost function, and the settled state is the pattern where that cost is zero. The T10 orbit-section module proves two limits on how that settled state can be selected.

The first limit concerns reformulations. The module proves that if a proposed constraint has exactly the same zero set as the load cost on all valid carriers, then imposing that constraint is literally the same as selecting the ground state, not a weaker law derived from it. A visible instance is any reparametrization f(loadCost) = 0 where f vanishes only at zero, which covers double-entry balance restatements. The second limit is sharper: any predicate on patterns that is merely closed under positive rescaling, meaning it cannot tell a pattern from a scaled copy, cannot be a realization predicate that satisfies the ground-state selection law, as soon as it accepts one valid carrier. The proof is a doubling counterexample: rescale the accepted carrier onto its orbit zero, then double, and the result is still accepted while sitting at ratio four, where the cost is nonzero.

These are not independence results about the whole foundation. The foundation is not scale-blind. The module 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. An independence claim quantified over the whole foundation would be false, and was refuted on 2026-07-27. Both no-go results carry witnesses showing their hypotheses are load-bearing: dropping the same-zero-set hypothesis lets R4 fail, and dropping the accepted-carrier hypothesis lets a trivial predicate satisfy R4.

What this means in plain language: the settled state cannot be found by looking only at a pattern's shape, ignoring its size. Any selection rule that is blind to scale either accepts too much, including patterns at ratio four with nonzero cost, or accepts nothing at all. The load must be allowed to see the actual amplitude, and the framework's derived occupancy predicate does exactly that.

THEOREM sameZeroSet_constraint_is_groundStateSelection · IndisputableMonolith/Masses/MassGenesis/T10OrbitSectionNoGo.lean
sameZeroSet_constraint_is_groundStateSelection · IndisputableMonolith/Masses/MassGenesis/T10OrbitSectionNoGo.lean:168 
/-- **No-go 1 (cosmetic reformulation).** Imposing any constraint with the load
cost's zero set on a realization predicate whose members are Q3 carriers is
logically the same act as adopting `RecognitionGroundStateSelection`.

The forward reading is the one that bites: a proposal that looks like an
equality law rather than a minimization principle, and which vanishes exactly
where the cost does, has not replaced R4. It has renamed it. The nontrivial
input is not the same-zero-set hypothesis, which only relates `C` to the cost at
a point; it is `orbitSection_groundStateSelection_pointwise`, which says an
inequality holding across a whole orbit is no weaker than an equation at one
point. -/
theorem sameZeroSet_constraint_is_groundStateSelection
    (C : LightPattern (Fin 8) → Prop)
    (hC : HasLoadCostZeroSetOnCarriers C)
    (Realized : LightPattern (Fin 8) → Prop)
    (hcarrier :
      ∀ ψ : LightPattern (Fin 8), Realized ψ → Q3ClosedPatternEvidence ψ) :
    (∀ ψ : LightPattern (Fin 8), Realized ψ → C ψ) ↔
      RecognitionGroundStateSelection Realized := by
  constructor
  · intro hall ψ hreal c hc
    have E := hcarrier ψ hreal
    exact
      (orbitSection_groundStateSelection_pointwise E).2
        ((hC ψ E).1 (hall ψ hreal)) c hc
  · intro hR4 ψ hreal
    have E := hcarrier ψ hreal
    exact
      (hC ψ E).2
        ((orbitSection_groundStateSelection_pointwise E).1
          (fun c hc => hR4 ψ hreal c hc))
THEOREM scaleBlindFragment_not_recognitionGroundStateSelection · IndisputableMonolith/Masses/MassGenesis/T10OrbitSectionNoGo.lean
scaleBlindFragment_not_recognitionGroundStateSelection · IndisputableMonolith/Masses/MassGenesis/T10OrbitSectionNoGo.lean:308 
/-- **No-go 2 (the scale-blind fragment floor).** No predicate on patterns that
is closed under positive rescaling can serve as a realization predicate
satisfying `RecognitionGroundStateSelection`, once it accepts a single Q3
carrier.

This generalizes `jointScaleInvariantSelector_does_not_force_amplitude` in three
directions: from amplitude selectors to arbitrary pattern predicates, from
invariance to mere closure, and from the amplitude equation to R4 itself. It
carries no emission-layer side condition.

**Scope.** The quantifier ranges over the rescaling-closed fragment, and that
fragment is proper: see `booleanOccupancy_is_derived_and_not_scaleBlind`. This
is therefore not an independence statement about the present foundation, and
must not be read or reported as one. -/
theorem scaleBlindFragment_not_recognitionGroundStateSelection
    (Realized : LightPattern (Fin 8) → Prop)
    (hP : IsRescalingClosedPatternPredicate Realized)
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hacc : Realized ψ) :
    ¬ RecognitionGroundStateSelection Realized := by
  intro hR4
  obtain ⟨χ, hPχ, ⟨Eχ⟩, hratio⟩ :=
    rescalingClosedPredicate_accepts_ratioFour_carrier Realized hP E hacc
  have hcost0 : loadRecognitionCost χ = 0 :=
    (orbitSection_groundStateSelection_pointwise Eχ).1
      (fun c hc => hR4 χ hPχ c hc)
  exact loadRecognitionCost_ne_zero_of_loadTopologyRatio_four hratio hcost0
THEOREM booleanOccupancy_is_derived_and_not_scaleBlind · IndisputableMonolith/Masses/MassGenesis/T10OrbitSectionNoGo.lean
booleanOccupancy_is_derived_and_not_scaleBlind · IndisputableMonolith/Masses/MassGenesis/T10OrbitSectionNoGo.lean:420 
/-- **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⟩
THEOREM booleanOccupancy_is_derived_and_not_scaleBlind · IndisputableMonolith/Masses/MassGenesis/T10OrbitSectionNoGo.lean
booleanOccupancy_is_derived_and_not_scaleBlind · IndisputableMonolith/Masses/MassGenesis/T10OrbitSectionNoGo.lean:420 
/-- **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⟩

What this page does not claim

This module does not prove that the whole foundation is scale-blind; it proves the opposite for the derived occupancy predicate. The no-go results do not show that no selection rule exists, only that rules blind to rescaling cannot work. The module does not derive the specific value of the settled amplitude beyond forcing it to one.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND