Encyclopedia Masses Masses Mass Genesis T10 Amplitude Equation Settled Anchor Amplitude Eq Of Load R

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Amplitude Equation Settled Anchor Amplitude Eq Of Load R

A single equation links the vanishing of a recognition cost to the exact amplitude of a settled pattern, and the proof stops short of saying any real pattern already satisfies it.

Verify this page

The amplitude equation

The declaration settledAnchor_amplitude_eq_of_loadRecognitionCost_zero is a theorem in the machine-checked library of formal theorems behind Recognition Science. It states a conditional result: if a pattern is a settled anchor with nonnegative amplitude, and if the load-recognition cost of that pattern is zero, then the amplitude equals the primitive positive-stationary factor amplitude. In plainer terms, the theorem says that the condition of zero cost pins down the amplitude exactly; there is no slack in the relationship.

The proof rests on two earlier equivalences. First, for a nonnegative settled anchor, load normalization holds if and only if the amplitude matches the primitive factor amplitude. Second, on a Q3 carrier, the load-recognition cost vanishes exactly when load normalization holds. Composing these two gives the direct implication: zero cost forces the amplitude equation. The theorem is the forward direction of the full equivalence, and it is what the certificate T10AmplitudeEquationCert records as its jcost_zero_iff_amplitude component.

What the theorem does not claim is just as important. Existence and uniqueness of a ground-state rescaling do not imply that the current representative already sits at the ground state. The library proves a countermodel: there exists a positive-amplitude settled Q3 carrier with a unique positive ground-state scale whose current amplitude is not the primitive factor amplitude. So the theorem is a conditional bridge, not an unconditional statement about any physical pattern. The physical premise that the settled representative itself has zero load-recognition cost remains open content, not a derived fact.

The practical consequence is that the amplitude equation is the same remaining physical statement as the vanishing of the cost. Neither follows from unit source magnitude, and the source-to-window interface is already proved impossible for the phase-borne settlement family. The theorem sharpens what must be supplied by a carrier law, and it does not pretend to supply that law itself.

THEOREM settledAnchor_amplitude_eq_of_loadRecognitionCost_zero · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean
settledAnchor_amplitude_eq_of_loadRecognitionCost_zero · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeEquation.lean:108 
/-- Conditional closure in direct form: once the physical settled
representative is known to sit at σ=0, its amplitude equation follows. -/
theorem settledAnchor_amplitude_eq_of_loadRecognitionCost_zero
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hwin : SettledAnchorWindow a ψ)
    (ha : 0 ≤ a)
    (hcost : loadRecognitionCost ψ = 0) :
    a = primitivePositiveStationaryFactorAmplitude ψ :=
  (settledAnchor_loadRecognitionCost_zero_iff_amplitude E hwin ha).1 hcost
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 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 settled pattern already has zero load-recognition cost. The theorem does not claim that the primitive factor amplitude is derived from a carrier law. The theorem does not claim that unit source magnitude supplies the zero-cost 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