Encyclopedia Masses Masses Mass Genesis T10 Residual Is Load Normalization Settled Anchor Amplitude

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Residual Is Load Normalization Settled Anchor Amplitude

A machine-checked theorem shows that one open problem about particle masses is the same equation as another, relocating the difficulty rather than solving it.

Verify this page

The load normalization bridge

In the Recognition Science framework, a particle's mass is not a free parameter but a prediction that emerges from a pattern of eight discrete recognition events. The framework's library of machine-checked theorems tracks two separate attempts to state this prediction. The first, called the T10 residual, says that a settled posting amplitude amplitude (a measure of the strength of a recognition event) should equal a topology factor amplitude derived from the pattern's shape. The second, called M7, says that the load at a single site in the pattern should equal one eighth of the predicted mass. These look like different claims about different quantities.

The theorem settledAnchor_amplitude_iff_siteMeaningLoad_eq_predictedMass_div_eight proves they are the same claim. On a settled anchor, where the pattern has reached a stable state, the amplitude equals the topology factor amplitude if and only if the site load equals the predicted mass divided by eight. The proof runs through two intermediate facts: a settled anchor's site load is exactly twice the amplitude squared, and the topology factor amplitude squared is one sixteenth of the predicted mass. Combining these, the amplitude condition and the load condition become two ways of writing the same equation. The theorem is an identification, not a new physical law.

What the theorem does not do is settle the underlying physics. The certificate that packages these results still carries the negation of the amplitude condition as a banked wall, meaning the residual problem is not discharged. The theorem relocates the difficulty from one form to another: it shows that solving the T10 amplitude problem is exactly the same task as solving the M7 load normalization problem. It does not solve either. The framework's own documentation states this plainly: relocation, not closure.

The practical consequence is a reduction in the number of independent open problems. Anyone working on the mass law can now treat the amplitude residual and the load normalization as a single target. A proof of one is a proof of the other, under the stated conditions of a positive settled anchor. The bridge also connects to a broader surface: under full eight-site support and uniform load, the anchor-site condition is exactly the support-averaged mass law load, and on a Q3 carrier this becomes mass law load realization. The chain of equivalences means the framework's mass prediction stands or falls as one unit, not as two separate bets.

THEOREM settledAnchor_amplitude_iff_siteMeaningLoad_eq_predictedMass_div_eight · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean
settledAnchor_amplitude_iff_siteMeaningLoad_eq_predictedMass_div_eight · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean:96 
/-- **Identification (iff).** For a positive settled-anchor amplitude, matching
the topology factor amplitude is exactly the statement that the anchor site
meaning load equals one eighth of the predicted mass. -/
theorem settledAnchor_amplitude_iff_siteMeaningLoad_eq_predictedMass_div_eight
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hwin : SettledAnchorWindow a ψ)
    (ha : 0 < a) :
    a = primitivePositiveStationaryFactorAmplitude ψ ↔
      siteMeaningLoad ψ 0 = predictedMass ψ / 8 := by
  have hload := settledAnchor_siteMeaningLoad_eq hwin
  have hsq := factorAmplitude_sq_eq_predictedMass_div_sixteen ψ
  have hfac_pos := factorAmplitude_pos ψ
  constructor
  · intro hamp
    rw [hload, hamp, hsq]
    ring
  · intro hsite
    have ha_sq : a ^ 2 = predictedMass ψ / 16 := by
      have : 2 * a ^ 2 = predictedMass ψ / 8 := by
        rw [← hload, hsite]
      have h2ne : (2 : ℝ) ≠ 0 := by norm_num
      have hgoal : a ^ 2 = (predictedMass ψ / 8) / 2 :=
        (eq_div_iff h2ne).2 (by simpa [mul_comm] using this)
      calc
        a ^ 2 = (predictedMass ψ / 8) / 2 := hgoal
        _ = predictedMass ψ / 16 := by ring
    have hsq_eq :
        a ^ 2 = primitivePositiveStationaryFactorAmplitude ψ ^ 2 := by
      rw [ha_sq, hsq]
    -- Both sides nonnegative, so equal squares give equal values.
    calc
      a = Real.sqrt (a ^ 2) := (Real.sqrt_sq ha.le).symm
      _ = Real.sqrt
            (primitivePositiveStationaryFactorAmplitude ψ ^ 2) := by
              rw [hsq_eq]
      _ = primitivePositiveStationaryFactorAmplitude ψ :=
            Real.sqrt_sq hfac_pos.le
THEOREM settledAnchor_siteMeaningLoad_eq · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean
settledAnchor_siteMeaningLoad_eq · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean:39 
/-- On a settled anchor at amplitude `a`, the meaning load at the pattern
anchor site `0` is exactly `2 a²`. This is `settledAnchor_neutralizedNormSq`
read through `siteMeaningLoad`. -/
theorem settledAnchor_siteMeaningLoad_eq
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hwin : SettledAnchorWindow a ψ) :
    siteMeaningLoad ψ 0 = 2 * a ^ 2 := by
  unfold siteMeaningLoad
  exact settledAnchor_neutralizedNormSq hwin
THEOREM factorAmplitude_sq_eq_predictedMass_div_sixteen · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean
factorAmplitude_sq_eq_predictedMass_div_sixteen · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean:51 
/-- The primitive positive-stationary factor amplitude is the positive square
root of one sixteenth of the topology-predicted mass. General in `ψ`. -/
theorem factorAmplitude_sq_eq_predictedMass_div_sixteen
    (ψ : LightPattern (Fin 8)) :
    primitivePositiveStationaryFactorAmplitude ψ ^ 2 =
      predictedMass ψ / 16 := by
  have hfactor := primitivePositiveStationaryFactorAmplitude_sq ψ
  have hclosed := primitiveClosedPatternAmplitude_sq ψ
  have hmass := primitiveClosedPatternAmplitude_sq_eq_predictedMass_div_eight ψ
  have htwice :
      2 * primitivePositiveStationaryFactorAmplitude ψ ^ 2 =
        predictedMass ψ / 8 := by
    calc
      2 * primitivePositiveStationaryFactorAmplitude ψ ^ 2 =
          primitiveAnchorSectorLoad ψ * primitivePhiTransport ψ := hfactor
      _ = primitiveClosedPatternAmplitude ψ ^ 2 := hclosed.symm
      _ = predictedMass ψ / 8 := hmass
  have h16 :
      16 * primitivePositiveStationaryFactorAmplitude ψ ^ 2 =
        predictedMass ψ := by
    have := congrArg (fun x : ℝ => (8 : ℝ) * x) htwice
    ring_nf at this ⊢
    exact this
  have h16ne : (16 : ℝ) ≠ 0 := by norm_num
  exact (eq_div_iff h16ne).2 (by rw [mul_comm]; exact h16)
THEOREM siteMeaningLoad_anchor_eq_avg_iff_supportAveragedMassLawLoad · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean
siteMeaningLoad_anchor_eq_avg_iff_supportAveragedMassLawLoad · IndisputableMonolith/Masses/MassGenesis/T10ResidualIsLoadNormalization.lean:136 
/-- Under eight-site support and uniform site load, the anchor-site condition
`siteMeaningLoad ψ 0 = predictedMass ψ / 8` is exactly
`SupportAveragedMassLawLoad ψ`. The card-8 hypothesis is kept explicit: it is
the arithmetic that turns the T10 `/8` share into the M7 support average.
(For `worldlinePattern` seeds and their positive scalings the card is 8 by
definition; see `scalePattern_gapOne_support_card` below.) -/
theorem siteMeaningLoad_anchor_eq_avg_iff_supportAveragedMassLawLoad
    (ψ : LightPattern (Fin 8))
    (hcard : ψ.support.card = 8)
    (h0 : (0 : Fin 8) ∈ ψ.support)
    (huni : UniformSiteMeaningLoad ψ) :
    siteMeaningLoad ψ 0 = predictedMass ψ / 8 ↔
      SupportAveragedMassLawLoad ψ := by
  constructor
  · intro hanchor x hx
    have huni_x := huni x hx 0 h0
    have hcardR : (ψ.support.card : ℝ) = 8 := by exact_mod_cast hcard
    calc
      siteMeaningLoad ψ x = siteMeaningLoad ψ 0 := huni_x
      _ = predictedMass ψ / 8 := hanchor
      _ = predictedMass ψ / (ψ.support.card : ℝ) := by rw [hcardR]
  · intro havg
    have hcardR : (ψ.support.card : ℝ) = 8 := by exact_mod_cast hcard
    calc
      siteMeaningLoad ψ 0 = predictedMass ψ / (ψ.support.card : ℝ) :=
        havg 0 h0
      _ = predictedMass ψ / 8 := by rw [hcardR]

What this page does not claim

The theorem does not prove that the amplitude condition actually holds for any physical pattern. The theorem does not derive the value of any particle mass. The theorem does not close the residual problem; it only identifies it with the load normalization problem.

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