Encyclopedia Masses Masses Mass Genesis T10 Amplitude Equation

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Amplitude Equation

The T10 amplitude equation fixes the one remaining scale in mass genesis: it names the exact amplitude a settled pattern must have to sit at zero recognition cost.

Verify this page

The amplitude equation

In the Recognition Science framework, a ledger (a discrete record of recognition events) assigns each pattern a cost, and the framework's central theorem forces that cost to take a specific form. The T10 amplitude equation is the final scalar condition in the mass-genesis chain: it says that a settled anchor pattern, one whose window has the gap-one shape, has zero load-recognition cost exactly when its amplitude equals a topology-selected value called the primitive positive-stationary factor amplitude.

Classically, the equation is a statement about normalization. For a nonnegative settled anchor, the load-normalization law holds if and only if the posting amplitude equals that primitive factor amplitude. The settled load itself is exactly twice the amplitude squared: a settled anchor at amplitude a has neutralized squared load 2a². On a Q3 carrier, a pattern type that carries the closed-pattern evidence, vanishing load-recognition cost is equivalent to the amplitude equation holding. This is the strongest unconditional connection from the current cost ledger: the statement σ=0 and the amplitude equation are the same remaining physical statement.

The module also identifies the primitive factor amplitude as the ground-state scale of a unit seed. Rescaling a settled anchor rescales its posting amplitude multiplicatively, while the primitive factor amplitude itself is invariant under window rescaling because it reads topology only. For a unit settled Q3 seed, a positive rescaling is a J-cost ground-state scale if and only if that scale equals the primitive factor amplitude. This identifies the unique scale selected by the existence-and-uniqueness theorem for positive ground-state scales.

The sharp wall is that uniqueness does not place the current pattern at the ground state. The module proves a countermodel: there exists a positive-amplitude settled Q3 carrier with a unique positive J-cost ground-state rescaling whose current amplitude is not the primitive factor amplitude. Therefore existence and uniqueness of a ground-state scale do not imply that the current representative already sits there. The first missing physical premise is exact: the physical settled representative itself must satisfy loadRecognitionCost ψ = 0, equivalently its identity rescaling is the positive ground state. Unit source magnitude does not supply this premise, because the source-to-window interface is already proved impossible for the phase-borne settlement family.

In plain language, the module proves that if a pattern is settled and sits at zero recognition cost, its amplitude is forced to a specific topology-determined value. But it also proves that being settled and having a unique ground-state rescaling does not by itself put the pattern at that value. The physical content that the actual representative is at σ=0 remains open, pending a carrier law.

THEOREM settledAnchor_loadNormalized_iff_amplitude · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean
settledAnchor_loadNormalized_iff_amplitude · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean:64 
/-- **Amplitude equation characterization.** For a nonnegative settled
anchor, the topology load-normalization law holds if and only if its posting
amplitude is the primitive positive-stationary factor amplitude. -/
theorem settledAnchor_loadNormalized_iff_amplitude
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hwin : SettledAnchorWindow a ψ)
    (ha : 0 ≤ a) :
    LoadNormalizedToTopology ψ ↔
      a = primitivePositiveStationaryFactorAmplitude ψ := by
  constructor
  · intro hload
    have hnorm := settledAnchor_neutralizedNormSq hwin
    have hclosed := primitiveClosedPatternAmplitude_sq ψ
    have hfactor := primitivePositiveStationaryFactorAmplitude_sq ψ
    have hfactor_nonneg :=
      primitivePositiveStationaryFactorAmplitude_nonneg ψ
    unfold LoadNormalizedToTopology AnchorPhasePrimitiveAmplitudeNorm at hload
    nlinarith
  · intro hamp
    unfold LoadNormalizedToTopology AnchorPhasePrimitiveAmplitudeNorm
    calc
      normSq8 (neutralize (ψ.window 0)) = 2 * a ^ 2 :=
        settledAnchor_neutralizedNormSq hwin
      _ = 2 * primitivePositiveStationaryFactorAmplitude ψ ^ 2 := by
        rw [hamp]
      _ = primitiveAnchorSectorLoad ψ * primitivePhiTransport ψ :=
        primitivePositiveStationaryFactorAmplitude_sq ψ
      _ = primitiveClosedPatternAmplitude ψ ^ 2 :=
        (primitiveClosedPatternAmplitude_sq ψ).symm
THEOREM settledAnchor_loadRecognitionCost_zero_iff_amplitude · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean
settledAnchor_loadRecognitionCost_zero_iff_amplitude · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean:94 
/-- On a Q3 carrier, the canonical load-recognition J-cost vanishes exactly
when the settled-anchor amplitude equation holds.  This is the strongest
unconditional connection from the current cost ledger: σ=0 and the amplitude
equation are the same remaining physical statement. -/
theorem settledAnchor_loadRecognitionCost_zero_iff_amplitude
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hwin : SettledAnchorWindow a ψ)
    (ha : 0 ≤ a) :
    loadRecognitionCost ψ = 0 ↔
      a = primitivePositiveStationaryFactorAmplitude ψ :=
  (loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology E).trans
    (settledAnchor_loadNormalized_iff_amplitude hwin ha)
THEOREM settledAnchor_neutralizedNormSq · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean
settledAnchor_neutralizedNormSq · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean:49 
/-- A settled anchor at amplitude `a` has neutralized squared load `2 a²`.
This is the scalar content of the gap-one settlement shape. -/
theorem settledAnchor_neutralizedNormSq
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hwin : SettledAnchorWindow a ψ) :
    normSq8 (neutralize (ψ.window 0)) = 2 * a ^ 2 := by
  rw [LightLanguage.Geometry.NeutralMeaningManifold.neutralize_of_neutral
    (ψ.window 0) (settledAnchor_neutral hwin)]
  rw [hwin, commitSettlementWindow_zero_eq_gapOne]
  simp [normSq8, gapOneTwoPhaseMode, Fin.sum_univ_eight,
    Complex.normSq_apply]
  ring
THEOREM unitSettled_positiveScaleGroundState_iff_primitiveAmplitude · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean
unitSettled_positiveScaleGroundState_iff_primitiveAmplitude · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean:143 
/-- **Ground-state scale identification.** For a unit settled Q3 seed, a
positive rescaling is a J-cost ground-state scale if and only if that scale is
the primitive positive-stationary factor amplitude.  This identifies the
unique scale selected by `positiveScaleGroundState_existsUnique` without
claiming that an arbitrary representative already sits there. -/
theorem unitSettled_positiveScaleGroundState_iff_primitiveAmplitude
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hunit : SettledAnchorWindow 1 ψ)
    (c : {x : ℝ // 0 < x}) :
    PositiveScaleGroundState ψ c ↔
      c.1 = primitivePositiveStationaryFactorAmplitude ψ := by
  have Escaled : Q3ClosedPatternEvidence (scalePattern c.1 ψ) :=
    scalePattern_q3ClosedEvidence c.1 c.2 E
  have hscaled : SettledAnchorWindow c.1 (scalePattern c.1 ψ) := by
    simpa using scalePattern_settledAnchor c.1 hunit
  have hiff :=
    settledAnchor_loadRecognitionCost_zero_iff_amplitude
      Escaled hscaled (le_of_lt c.2)
  rw [primitivePositiveStationaryFactorAmplitude_scalePattern] at hiff
  exact hiff
THEOREM uniqueGroundStateScale_does_not_force_currentAmplitude · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean
uniqueGroundStateScale_does_not_force_currentAmplitude · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean:185 
/-- **Scale-identification wall.** There exists a positive-amplitude settled
Q3 carrier with a unique positive J-cost ground-state rescaling whose CURRENT
amplitude is not the primitive factor amplitude.  Therefore existence and
uniqueness of a ground-state scale do not imply that the current
representative is already the ground state. -/
theorem uniqueGroundStateScale_does_not_force_currentAmplitude :
    ∃ (ψ : LightPattern (Fin 8)) (a : ℝ),
      0 < a ∧
      Q3MatterCarrier ψ ∧
      SettledAnchorWindow a ψ ∧
      (∃! c : {x : ℝ // 0 < x}, PositiveScaleGroundState ψ c) ∧
      a ≠ primitivePositiveStationaryFactorAmplitude ψ := by
  obtain ⟨Eseed⟩ := q3MatterCarrier_worldlinePattern_gapOne
  obtain ⟨c, hc, hload⟩ :=
    exists_scale_loadNormalizedToTopology Eseed
  let ground :=
    scalePattern c (worldlinePattern gapOneTwoPhaseMode)
  have Eground : Q3ClosedPatternEvidence ground := by
    exact scalePattern_q3ClosedEvidence c hc Eseed
  have hgroundCarrier : Q3MatterCarrier ground := ⟨Eground⟩
  have hgroundLoad : LoadNormalizedToTopology ground := by
    exact hload
  have hgroundWin : SettledAnchorWindow c ground := by
    simpa [ground] using
      scalePattern_settledAnchor c worldlineGapOne_settledAnchor
  let bad := scalePattern 2 ground
  have hwall :=
    q3MatterCarrier_underdetermines_loadNormalizedToTopology
      (ψ := ground) 2 (by norm_num) (by norm_num)
      hgroundCarrier hgroundLoad
  have hbadCarrier : Q3MatterCarrier bad := by
    simpa [bad] using hwall.1
  have hbadNotLoad : ¬ LoadNormalizedToTopology bad := by
    simpa [bad] using hwall.2.2
  have hbadWin : SettledAnchorWindow (2 * c) bad := by
    simpa [bad] using scalePattern_settledAnchor 2 hgroundWin
  have hbadPos : 0 < 2 * c := mul_pos (by norm_num) hc
  have hbadNe :
      2 * c ≠ primitivePositiveStationaryFactorAmplitude bad := by
    intro heq
    exact hbadNotLoad
      ((settledAnchor_loadNormalized_iff_amplitude
        hbadWin (le_of_lt hbadPos)).2 heq)
  refine ⟨bad, 2 * c, hbadPos, hbadCarrier, hbadWin, ?_, hbadNe⟩
  exact positiveScaleGroundState_existsUnique hbadCarrier

What this page does not claim

The module does not prove that any actual physical pattern satisfies the amplitude equation. The module does not derive the numerical value of the primitive factor amplitude for any specific particle. The module does not claim that a unique ground-state rescaling forces the current amplitude to be that ground state.

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