Masses Mass Genesis T10 Affine Section Shape Exists Unique Scale Mass Law Load R

A unique scale

The declaration exists_unique_scale_massLawLoadRealized_gapOne is a theorem in the Recognition Science library's formal, machine-checked collection. It concerns light patterns, which are discrete arrays of eight entries that represent a recognition event's structure. The theorem states that for a particular pattern called the gap-one worldline pattern, there exists exactly one positive number c such that rescaling the pattern by c makes it satisfy a condition called MassLawLoadRealized. In plain terms, among all possible uniform rescalings of this one pattern, precisely one scale makes a certain load-and-mass relationship hold.

The result is an instance of a more general theorem, exists_unique_scale_massLawLoadRealized, which applies to any nontrivially loaded pattern. The proof rests on two facts. First, the integrated meaning load of a pattern scales quadratically under rescaling, meaning it multiplies by c². Second, the predicted mass of a pattern is invariant under rescaling, meaning it stays the same. The theorem shows that when you subtract the invariant mass from the quadratically scaling load, the difference crosses zero at exactly one positive scale. This is the affine section shape: a quantity that can select a unique normalization.

This uniqueness is not a derivation of the normalization itself. The theorem proves that a unique scale exists, but it does not prove that a realized pattern sits at that scale. That statement remains open. The theorem also assumes the load is positive and nontrivial; it says nothing about orbits through the zero load. And it does not provide a candidate law for particle masses, only a shape that a candidate law must have.

/-- Non-vacuity of the concrete instantiation: the hypothesis is inhabited by
the campaign's own gap-one worldline pattern. -/
theorem exists_unique_scale_massLawLoadRealized_gapOne :
    ∃! c : ℝ, 0 < c ∧
      MassLawLoadRealized (scalePattern c (worldlinePattern gapOneTwoPhaseMode)) :=
  exists_unique_scale_massLawLoadRealized _ gapOne_nontrivialNeutralLoad

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

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 normalization; it only proves a unique scale exists. The theorem does not claim that any realized pattern sits at that unique scale. The theorem says nothing about orbits through the zero load, where the positivity assumptions fail.

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: