Masses Mass Genesis T10 Affine Section Shape

The shape of a scale selector

The T10 affine section shape module answers a precise question: what kind of quantity can select a unique scale for a pattern? In the Recognition Science framework, a ledger is a discrete record of posting events, and a pattern is a configuration of eight sites with support and topology. Rescaling a pattern by a positive factor c fixes its support and topology by definition, so the rescaling action never changes which sites are active or how they connect. The module asks which functions of a pattern can cut through the family of rescaled copies and name exactly one member as special.

The negative result is stark. A ledger cost that reads only the support and topology of a pattern is invariant under rescaling: every rescaled copy produces the same cost, so such a cost can never select a scale. The module proves this for both posting costs in the library, the L1 cost and the Jlog cost, and shows that the rescaling transition itself posts nothing. The deeper reason is a missing bridge: the rescaling action operates on patterns, while the ledger costs operate on ledger states, and the library contains no function connecting the two layers. Any future bridge that reads only support and topology will inherit the same blindness.

The positive half identifies one shape that can select a scale. If a quantity A scales as c² and a quantity B is scale-invariant, then the difference A − B vanishes at exactly one positive rescaling on each orbit. The module instantiates this with the library's own load: integratedMeaningLoad scales as c², while predictedMass is invariant. The theorem exists_unique_scale_massLawLoadRealized proves that exactly one positive rescaling of a nontrivially loaded pattern satisfies the mass law, and a concrete instance exists on the gap-one worldline pattern.

The contrast that makes the module discriminate is the equivariant case. A constraint of the form C(scalePattern c ψ) = ρ(c)·C(ψ) with ρ(c) ≠ 0 has a scale-saturated zero set: if it vanishes at one scale, it vanishes at all. Such a constraint cannot select a normalization. The affine difference of a degree-two term and an invariant term is the one shape that can.

The module does not derive the normalization itself. It proves that a unique scale exists on each orbit, not that a realized pattern sits at that scale. The ledger no-go is conditional on the reading being posting-count only, a hypothesis about a bridge that does not yet exist. The affine result assumes both terms are positive, so it says nothing about orbits through the zero load. The module characterizes the shape a candidate must have and rules out two shapes it must not have.

/-- **The consequence that matters.** No cost the ledger charges can be the
discriminating quantity in a normalization principle: on posting-count readings
it is constant along each orbit, and a quantity constant along an orbit cannot
cut a section of the orbit projection. -/
theorem ledgerCost_not_cutsScaleSection {d : Nat}
    (cost : LedgerPostingAdjacency.LedgerState d →
      LedgerPostingAdjacency.LedgerState d → ℝ)
    (read read' : LightPattern (Fin 8) → LedgerPostingAdjacency.LedgerState d)
    (hread : IsPostingCountReading read) (hread' : IsPostingCountReading read')
    (ψ : LightPattern (Fin 8)) :
    ¬ CutsScaleSectionAt (fun χ => cost (read χ) (read' χ)) ψ := by
  refine scaleInvariant_not_cutsScaleSection ?_
  intro c _
  exact ledgerCost_scalePattern_invariant cost read read' hread hread' c ψ

/-- **Fully concrete instantiation.** Exactly one positive rescaling of a
nontrivially loaded pattern realizes the mass law. This is an existence and
uniqueness statement about the orbit; it does not say that a realized pattern
sits at that scale, which is the open sentence. -/
theorem exists_unique_scale_massLawLoadRealized
    (ψ : LightPattern (Fin 8)) (hL : NontrivialNeutralLoad ψ) :
    ∃! c : ℝ, 0 < c ∧ MassLawLoadRealized (scalePattern c ψ) := by
  obtain ⟨c₀, ⟨hc₀, hz⟩, huniq⟩ :=
    exists_unique_scale_integratedMeaningLoad_eq ψ predictedMass
      (predictedMass_scaleInvariantAt ψ) (predictedMass_pos ψ) hL
  refine ⟨c₀, ⟨hc₀, ?_⟩, ?_⟩
  · have hz' :
        integratedMeaningLoad (scalePattern c₀ ψ)
          - predictedMass (scalePattern c₀ ψ) = 0 := hz
    show integratedMeaningLoad (scalePattern c₀ ψ) = predictedMass (scalePattern c₀ ψ)
    linarith
  · rintro c ⟨hc, hrz⟩
    refine huniq c ⟨hc, ?_⟩
    have hrz' :
        integratedMeaningLoad (scalePattern c ψ)
          = predictedMass (scalePattern c ψ) := hrz
    show integratedMeaningLoad (scalePattern c ψ)
        - predictedMass (scalePattern c ψ) = 0
    linarith

/-- **Fully concrete instantiation.** Exactly one positive rescaling of a
nontrivially loaded pattern realizes the mass law. This is an existence and
uniqueness statement about the orbit; it does not say that a realized pattern
sits at that scale, which is the open sentence. -/
theorem exists_unique_scale_massLawLoadRealized
    (ψ : LightPattern (Fin 8)) (hL : NontrivialNeutralLoad ψ) :
    ∃! c : ℝ, 0 < c ∧ MassLawLoadRealized (scalePattern c ψ) := by
  obtain ⟨c₀, ⟨hc₀, hz⟩, huniq⟩ :=
    exists_unique_scale_integratedMeaningLoad_eq ψ predictedMass
      (predictedMass_scaleInvariantAt ψ) (predictedMass_pos ψ) hL
  refine ⟨c₀, ⟨hc₀, ?_⟩, ?_⟩
  · have hz' :
        integratedMeaningLoad (scalePattern c₀ ψ)
          - predictedMass (scalePattern c₀ ψ) = 0 := hz
    show integratedMeaningLoad (scalePattern c₀ ψ) = predictedMass (scalePattern c₀ ψ)
    linarith
  · rintro c ⟨hc, hrz⟩
    refine huniq c ⟨hc, ?_⟩
    have hrz' :
        integratedMeaningLoad (scalePattern c ψ)
          = predictedMass (scalePattern c ψ) := hrz
    show integratedMeaningLoad (scalePattern c ψ)
        - predictedMass (scalePattern c ψ) = 0
    linarith

What this page does not claim

The module does not derive the normalization itself, only that a unique scale exists. The ledger no-go applies only to posting-count readings, not to all possible bridges. The affine result assumes both terms are positive and says nothing about zero load.

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