Encyclopedia Masses Masses Mass Genesis T10 Uniqueness Raw Anchor Unique Of Raw Canonical Positive S

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Uniqueness Raw Anchor Unique Of Raw Canonical Positive S

A machine-checked theorem pins down the first window of any light pattern that meets two conditions, while a broader uniqueness claim is known to be false.

Verify this page

The anchor uniqueness theorem

A light pattern, a discrete record of eight complex values arranged in a cycle, carries a topology and a first window. The theorem rawAnchor_unique_of_rawCanonicalPositiveStationary states that if two such patterns share the same topology and both satisfy a condition called raw canonical positive stationary, then their first windows are identical. The proof is short: the condition fixes the first window as a function of topology alone, so two patterns with equal topology must agree there.

The condition itself is a definitional choice, not a derived fact. A pattern is raw canonical positive stationary when its first window equals a specific primitive factor window, one built from a positive stationary amplitude that depends only on topology. The theorem does not show that any pattern must satisfy this condition; it shows only that if two patterns do, their first windows coincide. The machine-checked library of formal theorems records this as a proved statement, with the proof relying on a separate lemma that the primitive positive stationary amplitude is equal for patterns of the same topology.

This is the amplitude-rigidity part of a larger target called T10. The full target, pattern uniqueness over every stable closed light pattern, is false on the present carrier. Two distinct patterns, the gap-one mode and the gap-two mode, both generate valid carriers and each reaches a unique positive scale at which load cost is zero, yet they are not equivalent under the named physical orbit quotient. The library proves this separation by showing their phase-gap costs differ, six versus four, while orbit equivalence preserves phase-gap cost. So the honest summary is: the anchor theorem pins the first window under two hypotheses, but the broader pattern uniqueness remains open, and the raw target is refuted.

What the theorem changes is the shape of the remaining problem. Rigidity after the anchor mode is supplied is not the missing piece; the missing physics is the derivation of that mode and the topology restriction. A conditional rigidity theorem completes the picture: at fixed topology, window equivariance plus the raw canonical positive stationary anchor determine the entire light pattern, not just the first window. The open work is therefore to derive the anchor condition from more basic principles, not to patch the uniqueness proof.

THEOREM rawAnchor_unique_of_rawCanonicalPositiveStationary · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean
rawAnchor_unique_of_rawCanonicalPositiveStationary · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean:108 
/-- With the stronger raw canonical mode, fixed topology uniquely fixes the
unneutralized anchor window as well. -/
theorem rawAnchor_unique_of_rawCanonicalPositiveStationary
    {ψ χ : LightPattern (Fin 8)}
    (htop : ψ.topology = χ.topology)
    (hψ : AnchorPhaseRawCanonicalPositiveStationaryPrimitiveFactorMode ψ)
    (hχ : AnchorPhaseRawCanonicalPositiveStationaryPrimitiveFactorMode χ) :
    ψ.window 0 = χ.window 0 := by
  rw [hψ, hχ]
  unfold canonicalPositiveStationaryPrimitiveFactorWindow
  rw [primitivePositiveStationaryFactorAmplitude_eq_of_sameTopology htop]
THEOREM target_matter_is_unique_refuted · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean
target_matter_is_unique_refuted · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean:39 
/-- **T10 raw-target wall (THEOREM).** The placeholder raw `∃!` target is
false: the canonical seed and the existing tail counterexample are both stable
but are different light patterns. -/
theorem target_matter_is_unique_refuted :
    ¬ target_matter_is_unique := by
  rintro ⟨ψ, _hψ, hunique⟩
  have hseed : t10SeedPattern = ψ :=
    hunique t10SeedPattern t10SeedPattern_stable
  have htail : rawTailStableCounterexample = ψ :=
    hunique rawTailStableCounterexample rawTailStableCounterexample_stable
  have heq : t10SeedPattern = rawTailStableCounterexample :=
    hseed.trans htail.symm
  have hwindow :=
    congrArg (fun η : LightPattern (Fin 8) => η.window 0 0) heq
  simp [t10SeedPattern, t10SeedWindow, rawTailStableCounterexample,
    rawTailCounterexampleWindow] at hwindow
THEOREM exists_distinct_gapGroundStates · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean
exists_distinct_gapGroundStates · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean:302 
/-- Both inequivalent gap worldlines reach their own unique positive J-cost
ground-state scale, and those two ground-state patterns remain distinct. -/
theorem exists_distinct_gapGroundStates :
    ∃ c d : {x : ℝ // 0 < x},
      PositiveScaleGroundState (worldlinePattern gapOneTwoPhaseMode) c ∧
      PositiveScaleGroundState (worldlinePattern gapTwoTwoPhaseMode) d ∧
      scalePattern c.1 (worldlinePattern gapOneTwoPhaseMode) ≠
        scalePattern d.1 (worldlinePattern gapTwoTwoPhaseMode) := by
  obtain ⟨c, hc, _⟩ :=
    positiveScaleGroundState_existsUnique q3MatterCarrier_worldlinePattern_gapOne
  obtain ⟨d, hd, _⟩ :=
    positiveScaleGroundState_existsUnique q3MatterCarrier_worldlinePattern_gapTwo
  refine ⟨c, d, hc, hd, ?_⟩
  intro h
  have hwindow :=
    congrArg (fun ψ : LightPattern (Fin 8) => ψ.window 0 1) h
  have hcC : (c.1 : ℂ) = 0 := by
    simpa [scalePattern, worldlinePattern, gapOneTwoPhaseMode,
      gapTwoTwoPhaseMode] using hwindow
  have hcR : c.1 = 0 := by
    exact_mod_cast hcC
  exact (ne_of_gt c.2) hcR
THEOREM q3Pattern_unique_of_sameTopology_rawCanonicalPositiveStationary · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean
q3Pattern_unique_of_sameTopology_rawCanonicalPositiveStationary · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean:120 
/-- Fixed topology, Q3 worldline equivariance, and the raw canonical
positive-stationary anchor mode determine the entire light pattern. The theorem
is conditional on the raw mode; it does not derive that mode from the ledger. -/
theorem q3Pattern_unique_of_sameTopology_rawCanonicalPositiveStationary
    {ψ χ : LightPattern (Fin 8)}
    (Eψ : Q3ClosedPatternEvidence ψ)
    (Eχ : Q3ClosedPatternEvidence χ)
    (htop : ψ.topology = χ.topology)
    (hψ : AnchorPhaseRawCanonicalPositiveStationaryPrimitiveFactorMode ψ)
    (hχ : AnchorPhaseRawCanonicalPositiveStationaryPrimitiveFactorMode χ) :
    ψ = χ := by
  have h0 : ψ.window 0 = χ.window 0 :=
    rawAnchor_unique_of_rawCanonicalPositiveStationary htop hψ hχ
  have step_eq : ∀ x : Fin 8, ψ.window x = χ.window x →
      ψ.window (eightTickSupportStep x) =
        χ.window (eightTickSupportStep x) := by
    intro x hx
    rw [Eψ.window_equivariant x, Eχ.window_equivariant x, hx]
  have h1 : ψ.window 1 = χ.window 1 := by
    simpa [eightTickSupportStep] using step_eq 0 h0
  have h2 : ψ.window 2 = χ.window 2 := by
    simpa [eightTickSupportStep] using step_eq 1 h1
  have h3 : ψ.window 3 = χ.window 3 := by
    simpa [eightTickSupportStep] using step_eq 2 h2
  have h4 : ψ.window 4 = χ.window 4 := by
    simpa [eightTickSupportStep] using step_eq 3 h3
  have h5 : ψ.window 5 = χ.window 5 := by
    simpa [eightTickSupportStep] using step_eq 4 h4
  have h6 : ψ.window 6 = χ.window 6 := by
    simpa [eightTickSupportStep] using step_eq 5 h5
  have h7 : ψ.window 7 = χ.window 7 := by
    simpa [eightTickSupportStep] using step_eq 6 h6
  have hwindow : ψ.window = χ.window := by
    funext x
    fin_cases x <;> assumption
  have hsupport : ψ.support = χ.support :=
    Eψ.full_support.trans Eχ.full_support.symm
  cases ψ
  cases χ
  simp_all

What this page does not claim

The theorem does not show that any pattern must satisfy the raw canonical positive stationary condition. The theorem does not establish uniqueness of the full pattern, only of the first window. The broader T10 pattern-uniqueness target is not proved; it is refuted on the present carrier.

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/T10Uniqueness.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