Encyclopedia Masses Masses Mass Genesis T10 Amplitude Equation Primitive Positive Stationary Factor

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Amplitude Equation Primitive Positive Stationary Factor

A machine-checked theorem pins down the one scale at which a settled pattern's load vanishes, and proves that nothing else forces it there.

Verify this page

The amplitude equation

The declaration primitivePositiveStationaryFactorAmplitude_scalePattern belongs to a machine-checked library of formal theorems. It states that this quantity, the primitive positive-stationary factor amplitude, does not change when you rescale the window it describes. Rescaling means multiplying all the values in the window by a constant factor. The amplitude reads only the topology, the shape of the pattern, not its size. So the theorem says: scale the window up or down, and the amplitude stays put.

Why does that matter? In the Recognition Science framework, a ledger, a discrete record of events, assigns a cost to each pattern. The amplitude equation is the condition that this cost vanishes. The theorem proves that for a unit settled seed, meaning a pattern whose window has amplitude exactly one, a positive rescaling is a ground state, a configuration of lowest cost, exactly when that rescaling equals the primitive positive-stationary factor amplitude. In other words, the amplitude equation picks out the unique scale at which the load recognition cost hits zero. The settled load itself is exactly twice the amplitude squared, a separate theorem in the same module.

The declaration also proves a sharp wall. There exists a settled pattern with a unique positive ground-state rescaling whose current amplitude is not the primitive factor amplitude. Existence and uniqueness of a ground-state scale do not put the current representative there. The framework proves that if the physical settled representative satisfies the cost-vanishing condition, then its amplitude equation follows. But unit source magnitude alone does not supply that premise.

What the declaration does not claim is just as precise. It does not claim that an arbitrary current representative already sits at the ground state. It does not claim that the physical settled representative is a J-cost ground state; that remains open physical content until derived by a carrier law. The theorem is about the mathematics of scales and costs, not about which physical pattern actually occurs.

THEOREM primitivePositiveStationaryFactorAmplitude_scalePattern · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean
primitivePositiveStationaryFactorAmplitude_scalePattern · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean:135 
/-- The primitive positive-stationary factor amplitude is invariant under
window rescaling because it reads topology only. -/
theorem primitivePositiveStationaryFactorAmplitude_scalePattern
    (c : ℝ) (ψ : LightPattern (Fin 8)) :
    primitivePositiveStationaryFactorAmplitude (scalePattern c ψ) =
      primitivePositiveStationaryFactorAmplitude ψ :=
  primitivePositiveStationaryFactorAmplitude_eq_of_sameTopology rfl
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 declaration does not claim that an arbitrary current representative already sits at the ground state. The declaration does not claim that the physical settled representative is a J-cost ground state. The declaration does not claim that unit source magnitude supplies the cost-vanishing premise.

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