Masses Mass Genesis T10 Pattern Anchor Equality Settled Anchor Raw Canonical Mod

The settled anchor condition

A light pattern, a discrete record of eight phase values around a cycle, carries an anchor window: the first two entries of its eight-slot window. A settled anchor is the identification that this window equals the window posted by a settled commitment, scaled by a posting amplitude a. The framework's machine-checked library of formal theorems proves that, given this settled shape, the pattern's raw canonical positive-stationary mode holds if and only if the posting amplitude equals the pattern's primitive positive-stationary factor amplitude. In plain words: once you know the anchor window is a settled one, the only thing that can still fail is a single equality between two numbers, the posting amplitude and the pattern's own factor amplitude. Nothing else is missing.

The theorem, named settledAnchor_rawCanonicalMode_iff_amplitude, is an if-and-only-if statement. Its forward direction shows that if the raw canonical mode holds, then the amplitude equation must hold. Its reverse direction shows that if the amplitude equation holds, then the raw canonical mode follows. The proof is short: it uses the settled anchor's phase-zero value, which the library shows equals the posting amplitude, and the phase-one value, which equals its negative. The residual between settlement and the rigidity anchor premise is exactly the amplitude equation, nothing else.

This result matters because it supplies two of the four premises that the fixed-topology rigidity theorem needs: the ledger-to-photon tail-zero bridge and anchor neutrality both follow from the settled shape. The other two premises, a legal first-edge post and the amplitude equation, remain named inputs. The theorem does not claim that the primitive factor amplitude equals the unit posting amplitude; that equality is a separate matter. It also does not claim that every settled anchor satisfies the amplitude equation, only that the mode holds exactly when it does.

/-- **Pattern-anchor equality (sufficiency).** A settled anchor whose posting
amplitude satisfies the amplitude equation carries the raw canonical
positive-stationary mode. -/
theorem settledAnchor_rawCanonicalMode
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hwin : SettledAnchorWindow a ψ)
    (hamp : a = primitivePositiveStationaryFactorAmplitude ψ) :
    AnchorPhaseRawCanonicalPositiveStationaryPrimitiveFactorMode ψ := by
  apply rawCanonicalPositiveStationaryMode_of_components
  refine ⟨?_, ?_, settledAnchor_tail_zero hwin⟩
  · rw [settledAnchor_phase0 hwin, hamp]
  · rw [settledAnchor_phase1 hwin, hamp]

/-- **The residual is exactly the amplitude equation.** For a settled
anchor, the raw canonical mode holds if and only if the posting amplitude
equals the primitive positive-stationary factor amplitude. Nothing else is
missing between settlement and the rigidity anchor premise. -/
theorem settledAnchor_rawCanonicalMode_iff_amplitude
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hwin : SettledAnchorWindow a ψ) :
    AnchorPhaseRawCanonicalPositiveStationaryPrimitiveFactorMode ψ ↔
      a = primitivePositiveStationaryFactorAmplitude ψ := by
  constructor
  · intro hmode
    have hcomp := components_of_rawCanonicalPositiveStationaryMode ψ hmode
    have h0 := hcomp.phase0_amplitude
    rw [settledAnchor_phase0 hwin] at h0
    exact_mod_cast h0
  · exact settledAnchor_rawCanonicalMode hwin

/-- **The ledger-to-photon support bridge is supplied.** The tail-zero
premise named as "the missing ledger-to-photon support bridge" in
`T10RawModeSourceData` holds for every settled anchor. -/
theorem settledAnchor_tail_zero
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hwin : SettledAnchorWindow a ψ) :
    ∀ i : Fin 8, i.val ≠ 0 → i.val ≠ 1 → ψ.window 0 i = 0 := by
  intro i h0 h1
  rw [hwin]
  show (a : ℂ) * commitSettlementWindow 0 i = 0
  rw [commitSettlementWindow_adjacentPairSupport 0 i
    (fun h => h0 (by rw [h]; rfl))
    (fun h => h1 (by rw [h]; rfl)), mul_zero]

/-- Settlement neutrality transports to the pattern anchor. -/
theorem settledAnchor_neutral
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hwin : SettledAnchorWindow a ψ) :
    IsNeutral (ψ.window 0) := by
  unfold IsNeutral
  rw [hwin]
  show (∑ t : Fin 8, (a : ℂ) * commitSettlementWindow 0 t) = 0
  rw [← Finset.mul_sum]
  have hneutral := commitSettlementWindow_neutral 0
  unfold IsNeutral at hneutral
  rw [hneutral, mul_zero]

What this page does not claim

The primitive factor amplitude equals the unit posting amplitude. Every settled anchor satisfies the amplitude equation. The settled anchor identification itself is derived, rather than named as an input.

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/T10PatternAnchorEquality.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: