Encyclopedia Masses Masses Mass Genesis T10 Amplitude Equation Unit Settled Positive Scale Ground St

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Amplitude Equation Unit Settled Positive Scale Ground St

In Recognition Science, a unit-seeded settled pattern has exactly one preferred rescaling, and that scale is fixed by the pattern's topology alone.

Verify this page

The unique ground-state scale

In Recognition Science, a ledger (a discrete record of events) assigns a cost to every pattern of recognition events. A settled pattern is one whose internal structure has reached a stable, gap-one shape. The declaration unitSettled_positiveScaleGroundState_iff_primitiveAmplitude is a theorem in the framework's machine-checked library of formal theorems. It states that for a settled pattern with unit amplitude, a positive rescaling is a ground-state scale, meaning it minimizes the recognition cost, if and only if that scale equals a quantity called the primitive positive-stationary factor amplitude.

That quantity is not an arbitrary number. It is determined entirely by the pattern's topology, its connectivity structure, and not by its current size or amplitude. The theorem proves that the topology amplitude is the unique ground-state rescaling of the unit settlement window. In plain terms, if you start with a pattern whose amplitude is 1 and ask what single rescaling makes it a cost minimum, the answer is forced: it must be exactly this topology-selected amplitude. No other positive scale works.

The theorem also proves the converse direction. If a positive scale is a ground-state scale for a unit settled pattern, then that scale must equal the primitive factor amplitude. This is a sharp two-way equivalence. The framework's library shows that on a Q3 carrier, a class of patterns with a specific closed structure, the recognition cost vanishes exactly when this amplitude equation holds. So the amplitude equation and the condition of zero cost are the same remaining physical statement.

What the theorem does not claim is equally important. It does not say that any arbitrary pattern you happen to have is already sitting at its ground state. The library proves a countermodel: there exists a settled Q3 carrier 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 imply that the current representative is already the ground state. The physical premise that the actual settled representative satisfies the zero-cost condition remains open content, not a proved theorem.

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 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 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 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 theorem does not claim that any arbitrary pattern is already at its ground state. The theorem does not claim that the physical settled representative satisfies the zero-cost condition. The theorem does not derive the value of the primitive factor amplitude from first principles.

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