Encyclopedia Masses Masses Mass Genesis T10 Residual Is Load Normalization Settled Anchor Q3 Amplitu

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Residual Is Load Normalization Settled Anchor Q3 Amplitu

A machine-checked theorem shows that two different ways of describing a settled pattern's mass are the same equation, but it does not prove the mass itself is right.

Verify this page

The load-normalization identification

In the Recognition Science framework, a pattern's mass is not a single number but a distribution across eight sites. The framework's library, a machine-checked collection of formal theorems, tracks two descriptions of that distribution. One description looks at the pattern's amplitude, a positive number that sets its overall scale. The other looks at the load, the amount of meaning-weight each site carries. The theorem settledAnchor_q3_amplitude_iff_massLawLoadRealized proves that, on a settled pattern with all eight sites active and uniform load, these two descriptions coincide exactly: the amplitude matches a topology-predicted value if and only if the site load equals one eighth of the predicted mass.

The identification is an equivalence, not a new physical law. It says two previously separate statements, the T10 amplitude residual and the M7 mass-law load realization, are the same equation viewed from opposite sides. The proof runs through a chain of lemmas: the site load at the anchor is twice the amplitude squared; the topology factor amplitude squared is one sixteenth of the predicted mass; matching that amplitude is equivalent to the site load equaling one eighth of the predicted mass. Under the eight-site support and uniform-load conditions, that site condition is exactly the support-averaged load law. The certificate bundles these steps into a single theorem, with no unproved assumptions and no new axioms.

The theorem is an identification, not a resolution. It relocates the residual, the gap between the posted amplitude and the topology factor, to the mass-law load-normalization problem. The residual itself is still not discharged: the certificate explicitly carries the negation of the amplitude-matching statement via the banked wall. In plain terms, the framework has shown that two ways of describing the same pattern agree with each other, but it has not shown that either description matches any measured particle mass. The gap-one seed pattern, the concrete example used, does occupy all eight sites, and positive scalings preserve that support, so the conditions of the theorem are met for that case.

What this changes is the shape of the open problem. Instead of two separate residuals to chase, one in the amplitude and one in the load, the framework now has a single target: the mass-law load normalization. If the load is right, the amplitude is right, and vice versa. The remaining question is whether that shared condition holds for real particles, which is an empirical check against measured masses, not a theorem. The identification narrows the search space without claiming the search is over.

THEOREM settledAnchor_q3_amplitude_iff_massLawLoadRealized · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean
settledAnchor_q3_amplitude_iff_massLawLoadRealized · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean:229 
/-- Q3 closed evidence supplies the uniform-load and membership hypotheses, so
on a positive settled Q3 carrier the residual is exactly mass-law load
realization. Card 8 remains explicit. -/
theorem settledAnchor_q3_amplitude_iff_massLawLoadRealized
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hwin : SettledAnchorWindow a ψ)
    (ha : 0 < a)
    (hcard : ψ.support.card = 8) :
    a = primitivePositiveStationaryFactorAmplitude ψ ↔
      MassLawLoadRealized ψ := by
  have h0 : (0 : Fin 8) ∈ ψ.support := by
    rw [E.full_support]
    exact Finset.mem_univ 0
  have huni : UniformSiteMeaningLoad ψ := E.uniform_site_load
  have hnonempty : ψ.support.Nonempty := E.stable.1
  exact settledAnchor_amplitude_iff_massLawLoadRealized
    hwin ha hcard h0 huni hnonempty
THEOREM settledAnchor_amplitude_iff_massLawLoadRealized · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean
settledAnchor_amplitude_iff_massLawLoadRealized · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean:180 
/-- Under the same hypotheses, the residual is exactly `MassLawLoadRealized`:
the support-averaged surface realizes the integrated load law. -/
theorem settledAnchor_amplitude_iff_massLawLoadRealized
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hwin : SettledAnchorWindow a ψ)
    (ha : 0 < a)
    (hcard : ψ.support.card = 8)
    (h0 : (0 : Fin 8) ∈ ψ.support)
    (huni : UniformSiteMeaningLoad ψ)
    (hnonempty : ψ.support.Nonempty) :
    a = primitivePositiveStationaryFactorAmplitude ψ ↔
      MassLawLoadRealized ψ := by
  constructor
  · intro hamp
    have havg :
        SupportAveragedMassLawLoad ψ :=
      (settledAnchor_amplitude_iff_supportAveragedMassLawLoad
        hwin ha hcard h0 huni).1 hamp
    exact supportAveragedMassLawLoad_realizes ψ hnonempty havg
  · intro hrealized
    -- From MassLawLoadRealized + uniform + card 8, recover the average.
    have hsum :
        integratedMeaningLoad ψ = predictedMass ψ := hrealized
    rw [integratedMeaningLoad_eq_support_sum ψ] at hsum
    have hcardR : (ψ.support.card : ℝ) = 8 := by exact_mod_cast hcard
    have hcard_ne : (ψ.support.card : ℝ) ≠ 0 := by
      exact_mod_cast Finset.card_ne_zero.mpr hnonempty
    have havg_val :
        siteMeaningLoad ψ 0 = predictedMass ψ / 8 := by
      have hconst :
          ψ.support.sum (fun x => siteMeaningLoad ψ x) =
            ψ.support.sum (fun _x => siteMeaningLoad ψ 0) := by
        apply Finset.sum_congr rfl
        intro x hx
        exact huni x hx 0 h0
      have hsum0 :
          ψ.support.sum (fun _x => siteMeaningLoad ψ 0) =
            (ψ.support.card : ℝ) * siteMeaningLoad ψ 0 := by
        simp
      have : (ψ.support.card : ℝ) * siteMeaningLoad ψ 0 = predictedMass ψ := by
        rw [← hsum0, ← hconst, hsum]
      have : siteMeaningLoad ψ 0 =
          predictedMass ψ / (ψ.support.card : ℝ) :=
        (eq_div_iff hcard_ne).2 (by rw [mul_comm]; exact this)
      rw [this, hcardR]
    exact
      (settledAnchor_amplitude_iff_siteMeaningLoad_eq_predictedMass_div_eight
        hwin ha).2 havg_val
THEOREM T10ResidualIsLoadNormalizationCert · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean
T10ResidualIsLoadNormalizationCert · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean:273 
structure T10ResidualIsLoadNormalizationCert : Prop where
  settled_anchor_site_load :
    ∀ {a : ℝ} {ψ : LightPattern (Fin 8)},
      SettledAnchorWindow a ψ →
        siteMeaningLoad ψ 0 = 2 * a ^ 2
  factor_amplitude_sq :
    ∀ ψ : LightPattern (Fin 8),
      primitivePositiveStationaryFactorAmplitude ψ ^ 2 =
        predictedMass ψ / 16
  amplitude_iff_anchor_site_load :
    ∀ {a : ℝ} {ψ : LightPattern (Fin 8)},
      SettledAnchorWindow a ψ → 0 < a →
        (a = primitivePositiveStationaryFactorAmplitude ψ ↔
          siteMeaningLoad ψ 0 = predictedMass ψ / 8)
  anchor_site_iff_support_averaged :
    ∀ (ψ : LightPattern (Fin 8)),
      ψ.support.card = 8 →
        (0 : Fin 8) ∈ ψ.support →
          UniformSiteMeaningLoad ψ →
            (siteMeaningLoad ψ 0 = predictedMass ψ / 8 ↔
              SupportAveragedMassLawLoad ψ)
  amplitude_iff_mass_law_on_q3 :
    ∀ {a : ℝ} {ψ : LightPattern (Fin 8)},
      Q3ClosedPatternEvidence ψ →
        SettledAnchorWindow a ψ → 0 < a →
          ψ.support.card = 8 →
            (a = primitivePositiveStationaryFactorAmplitude ψ ↔
              MassLawLoadRealized ψ)
  gap_one_scaled_support_card :
    ∀ a : ℝ,
      (scalePattern a (worldlinePattern gapOneTwoPhaseMode)).support.card = 8
  residual_still_false : ¬ PostedAmplitudeMatchesTopologyFactor
THEOREM scalePattern_gapOne_support_card · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean
scalePattern_gapOne_support_card · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean:260 
/-- Positive scalings preserve support, so the settled factor-scaled gap-one
pattern likewise has eight support sites. -/
theorem scalePattern_gapOne_support_card (a : ℝ) :
    (scalePattern a (worldlinePattern gapOneTwoPhaseMode)).support.card = 8 := by
  simp [scalePattern, worldlineGapOne_support_card]

What this page does not claim

The theorem does not prove that any pattern's mass matches a measured particle value. The theorem does not discharge the residual; it only relocates it to the load-normalization problem. The theorem does not apply to patterns with fewer than eight active sites or non-uniform site loads.

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/T10ResidualIsLoadNormalization.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