Encyclopedia Masses Masses Mass Genesis T10 Pattern Anchor Equality

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Pattern Anchor Equality

A theorem showing that two light patterns with the same shape must be identical, provided their anchor points are set to the right amplitude.

Verify this page

Pattern anchor equality

A light pattern is a discrete record of eight values, one for each step in a recognition cycle. Its anchor is the first value in that record. The pattern anchor equality theorem states a rigidity result: if two closed patterns have the same topology, and each has an anchor that is a settled window at the correct posting amplitude, then the two patterns are equal. The name pattern anchor equality comes from this conclusion: the anchor, together with the settled shape, forces the whole pattern to be unique.

The theorem is proved in a machine-checked library of formal theorems. The proof connects a settled anchor to the raw canonical positive-stationary mode, a specific structural condition on the pattern. The key step is an equivalence: for a settled anchor, the raw canonical mode holds if and only if the posting amplitude equals the pattern's primitive positive-stationary factor amplitude. This means the only remaining condition between settlement and rigidity is exactly that amplitude equation, nothing else.

The module also supplies the missing ledger-to-photon support bridge, a premise that was previously absent. For any settled anchor, the tail values of the pattern are zero, and the anchor is neutral, meaning its values sum to zero. These properties are derived from the settled shape itself, not assumed separately.

In Recognition Science, this result establishes that matter-pattern rigidity fires from settlement data plus the amplitude equation alone. Two patterns with the same topology and settled anchors at the correct amplitude cannot differ. The theorem is a certificate that the named source interface is inhabited and that per-topology rigidity follows from the settled shape.

The honest scope is explicit: the identification that a pattern's anchor window is what one settled commitment posts is carried in the shape, but the identification itself and the amplitude equation remain two named inputs. No claim is made that the primitive factor amplitude equals the unit posting amplitude.

THEOREM q3Pattern_unique_of_sameTopology_settledAnchor · IndisputableMonolith/Masses/MassGenesis/T10PatternAnchorEquality.lean
q3Pattern_unique_of_sameTopology_settledAnchor · IndisputableMonolith/Masses/MassGenesis/T10PatternAnchorEquality.lean:176 
/-- **Rigidity from settlement.** Two Q3-closed patterns with the same
topology whose anchors are settled windows satisfying the amplitude
equation are EQUAL. Matter-pattern rigidity now fires from settlement data
plus the amplitude equation alone. -/
theorem q3Pattern_unique_of_sameTopology_settledAnchor
    {ψ χ : LightPattern (Fin 8)}
    (Eψ : Q3ClosedPatternEvidence ψ)
    (Eχ : Q3ClosedPatternEvidence χ)
    (htop : ψ.topology = χ.topology)
    {a b : ℝ}
    (hψwin : SettledAnchorWindow a ψ)
    (hχwin : SettledAnchorWindow b χ)
    (hψamp : a = primitivePositiveStationaryFactorAmplitude ψ)
    (hχamp : b = primitivePositiveStationaryFactorAmplitude χ) :
    ψ = χ :=
  q3Pattern_unique_of_sameTopology_rawCanonicalPositiveStationary
    Eψ Eχ htop
    (settledAnchor_rawCanonicalMode hψwin hψamp)
    (settledAnchor_rawCanonicalMode hχwin hχamp)
THEOREM settledAnchor_rawCanonicalMode_iff_amplitude · IndisputableMonolith/Masses/MassGenesis/T10PatternAnchorEquality.lean
settledAnchor_rawCanonicalMode_iff_amplitude · IndisputableMonolith/Masses/MassGenesis/T10PatternAnchorEquality.lean:141 
/-- **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
THEOREM settledAnchor_tail_zero · settledAnchor_neutral · IndisputableMonolith/Masses/MassGenesis/T10PatternAnchorEquality.lean
settledAnchor_tail_zero · IndisputableMonolith/Masses/MassGenesis/T10PatternAnchorEquality.lean:99 
/-- **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]
settledAnchor_neutral · IndisputableMonolith/Masses/MassGenesis/T10PatternAnchorEquality.lean:113 
/-- 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]
THEOREM settledAnchor_tail_zero · IndisputableMonolith/Masses/MassGenesis/T10PatternAnchorEquality.lean
settledAnchor_tail_zero · IndisputableMonolith/Masses/MassGenesis/T10PatternAnchorEquality.lean:99 
/-- **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]

What this page does not claim

The theorem does not claim that the primitive factor amplitude equals the unit posting amplitude. The theorem does not identify which specific posting amplitude occurs in nature. The theorem does not prove that every light pattern has a settled anchor.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND