Encyclopedia Masses Masses Mass Genesis T10 Amplitude Equation Unique Ground State Scale Does Not Fo

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Amplitude Equation Unique Ground State Scale Does Not Fo

A machine-checked theorem shows that knowing the one correct rescaling of a pattern is not the same as already being at that scale.

Verify this page

The unique scale wall

The declaration uniqueGroundStateScale_does_not_force_currentAmplitude is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It states, in plain terms, that a mathematical object can have exactly one preferred rescaling, a unique ground-state scale, while its current amplitude is not that preferred value. The theorem exhibits a concrete example: a settled anchor with positive amplitude, a Q3 matter carrier, which has a unique positive ground-state scale, yet whose current amplitude differs from the primitive positive-stationary factor amplitude. This is a sharp boundary result, not a vague caveat.

The theorem's content is best understood against what precedes it. Earlier results in the same module prove that, for a unit settled seed, a positive rescaling is a ground-state scale if and only if that scale equals the primitive positive-stationary factor amplitude. That is, the framework proves that the unique preferred scale is the one selected by the topology of the pattern. The wall theorem then shows the limit of that identification: existence and uniqueness of the ground-state scale do not imply that the current representative already sits at that scale. The example pattern satisfies all the structural conditions, has a unique ground-state rescaling, but is not itself at the ground state.

In Recognition Science, this distinction matters for the physical interpretation of the amplitude equation. The framework models a settled anchor at amplitude a as having neutralized squared load 2a². The amplitude equation, loadRecognitionCost ψ = 0, is equivalent to the amplitude being the primitive positive-stationary factor amplitude. The wall theorem does not establish that equation; it establishes that the equation is not automatically satisfied by any pattern that merely has a unique ground-state scale. The physical premise that the actual representative satisfies the amplitude equation remains open content, not a derived consequence.

The theorem also clarifies what is not being claimed. It does not say that the amplitude equation is false, nor that the ground-state scale is ill-defined. It says precisely that the current amplitude of a pattern is not forced to equal the unique ground-state scale merely because that scale exists and is unique. The framework's own docstring states this directly: uniqueness of that rescaling does not say that an arbitrary current representative is already at the ground state. The missing physical premise is exact: the physical settled representative itself must satisfy loadRecognitionCost ψ = 0.

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

What this page does not claim

The amplitude equation is false or unattainable. The unique ground-state scale is ill-defined or non-unique. The physical settled representative is already at the 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