Masses Mass Genesis T10 Affine Section Shape Exists Unique Scale Integrated Mean

The unique scale

The declaration exists_unique_scale_integratedMeaningLoad_eq is a machine-checked theorem in the Recognition Science framework's library of formal theorems. It concerns patterns, which are discrete configurations of eight sites, each carrying a complex number. The theorem states that for any pattern with a nontrivial load, and for any positive, scale-invariant quantity associated with it, there is exactly one positive rescaling of the pattern that makes the pattern's integrated meaning load equal that quantity. In plainer terms, if you have a measure that grows with the square of the scale, and another that does not change with scale, then there is precisely one zoom level at which the two match.

The theorem is a positive result in a broader investigation into how a scale could be selected. The library also proves a negative result: a constraint that merely scales with the pattern, without the affine subtraction, cannot select a scale. This is because its zero set is spread across all scales, not concentrated at one. The positive theorem, by contrast, shows that the difference between a scale-covariant quantity and a scale-invariant one has a zero set that cuts through each rescaling orbit at exactly one point. This is the shape a normalization principle must have to be able to pick out a scale at all.

The theorem is instantiated with the library's own definitions. The integrated meaning load is a degree-two quantity under rescaling, while the predicted mass is invariant. The theorem therefore proves that for any nontrivially loaded pattern, there is a unique positive rescaling that satisfies the mass law load realized condition. A concrete instance is provided for a specific gap-one worldline pattern. This is a structural result: it characterizes the shape a candidate law must have, and rules out two shapes it must not have.

What the theorem does not claim is just as important. It does not derive the actual normalization, meaning it does not say that a realized pattern sits at that unique scale. That remains an open sentence. The theorem also does not connect the pattern layer to the ledger layer, which is a separate, missing bridge in the library. The theorem assumes the quantities involved are positive, so it says nothing about orbits through zero load. It is a constraint on future bridges and candidate laws, not a statement about a present one.

/-- **Instantiated affine result.** Against the real integrated load: for any
positive scale-invariant reference `B`, exactly one positive rescaling of a
nontrivially loaded pattern sends the load to that reference. -/
theorem exists_unique_scale_integratedMeaningLoad_eq
    (ψ : LightPattern (Fin 8)) (B : LightPattern (Fin 8) → ℝ)
    (hB : ScaleInvariantAt B ψ) (hBpos : 0 < B ψ)
    (hL : NontrivialNeutralLoad ψ) :
    CutsScaleSectionAt (fun χ => integratedMeaningLoad χ - B χ) ψ :=
  affine_cutsScaleSection_deg_two integratedMeaningLoad B ψ
    (integratedMeaningLoad_covariantAt ψ) hB
    (integratedMeaningLoad_pos_of_nontrivial ψ hL) hBpos

/-- **The discriminating pair.** On one orbit: the affine constraint cuts a
section, while neither the covariant term alone nor the invariant term alone
can. A module proving only the first clause would not discriminate. -/
theorem affine_cuts_where_equivariant_cannot
    (ψ : LightPattern (Fin 8)) (hL : NontrivialNeutralLoad ψ) :
    CutsScaleSectionAt (fun χ => integratedMeaningLoad χ - predictedMass χ) ψ ∧
      ¬ CutsScaleSectionAt integratedMeaningLoad ψ ∧
        ¬ CutsScaleSectionAt predictedMass ψ := by
  refine
    ⟨exists_unique_scale_integratedMeaningLoad_eq ψ predictedMass
        (predictedMass_scaleInvariantAt ψ) (predictedMass_pos ψ) hL, ?_, ?_⟩
  · refine equivariant_not_cutsScaleSection (ρ := fun c => c ^ 2) ?_ ?_
    · intro c _
      exact integratedMeaningLoad_scalePattern c ψ
    · intro c hc
      exact pow_ne_zero 2 (ne_of_gt hc)
  · exact scaleInvariant_not_cutsScaleSection (predictedMass_scaleInvariantAt ψ)

theorem integratedMeaningLoad_covariantAt (ψ : LightPattern (Fin 8)) :
    ∀ c : ℝ, 0 < c →
      integratedMeaningLoad (scalePattern c ψ) = c ^ 2 * integratedMeaningLoad ψ :=
  fun c _ => integratedMeaningLoad_scalePattern c ψ

/-- The predicted mass reads only topology-derived labels, and rescaling copies
the topology, so it is scale-invariant by definitional equality. -/
theorem predictedMass_scalePattern (c : ℝ) (ψ : LightPattern (Fin 8)) :
    predictedMass (scalePattern c ψ) = predictedMass ψ := rfl

What this page does not claim

The theorem does not derive the actual normalization or say that a realized pattern sits at the unique scale. The theorem does not connect the pattern layer to the ledger layer. The theorem says nothing about orbits through 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: