Encyclopedia Masses Masses Mass Genesis T10 Uniqueness

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Uniqueness

A theorem that aimed to prove matter patterns are unique turns out to be false, and the corrected result is a sharper statement about what actually is unique.

Verify this page

The uniqueness wall

In Recognition Science, the T10 uniqueness target was meant to show that a stable pattern of matter, a ledger (a discrete record of events), is the only one possible. The machine-checked library of formal theorems, the framework's library, now contains a proof that this raw target is false. The proof, target_matter_is_unique_refuted, shows that the existing tail pattern is a second stable pattern. Stability, as currently defined, only requires locality plus a positive neutral load, and that definition is too weak to force a single pattern.

The failure is not the end of the story. The framework's library proves a corrected statement, positiveScaleGroundState_existsUnique: on a Q3 carrier, the canonical J-cost selects exactly one positive rescaling at which the load is normalized to topology. This is the amplitude-rigidity part of T10. It means that while the pattern itself is not unique, the scale at which it sits is rigid. The proof shows that for any valid Q3 matter carrier, there exists a unique positive scaling factor that makes the load recognition cost zero.

The library also proves a conditional rigidity theorem, q3Pattern_unique_of_sameTopology_rawCanonicalPositiveStationary. At fixed topology, if you also have the raw canonical positive-stationary anchor mode, then the entire pattern is determined. The missing physics is therefore not rigidity after these conditions are supplied; it is the derivation of that anchor mode and the topology restriction. These remain open targets.

The distinction between the two gap modes shows why the raw target fails. The library proves gapOne_rhatQuotient_ne_gapTwo: the gap-one and gap-two modes are in different Rhat quotient classes, so they cannot be identified by the named physical quotient. Each reaches a unique positive ground-state scale, but they are genuinely different patterns. Deriving an additional ledger selector or a stronger carrier that excludes one class remains open.

The practical consequence is a sharper division of labor. The framework has proved what is rigid: scale and, conditionally, the full pattern given the right anchor. What it has not proved is that the anchor itself is forced. That is the open problem, and the library states it plainly rather than pretending the raw target holds.

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 positiveScaleGroundState_existsUnique · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean
positiveScaleGroundState_existsUnique · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean:64 
/-- **T10 amplitude rigidity (THEOREM).** Every Q3 carrier has exactly one
positive scale in its scale orbit at which the canonical load-recognition
J-cost vanishes. -/
theorem positiveScaleGroundState_existsUnique
    {ψ : LightPattern (Fin 8)} (hcarrier : Q3MatterCarrier ψ) :
    ∃! c : {x : ℝ // 0 < x}, PositiveScaleGroundState ψ c := by
  obtain ⟨E⟩ := hcarrier
  obtain ⟨c, hc, hground⟩ := exists_scale_loadNormalizedToTopology E
  obtain ⟨Eground⟩ := scalePattern_q3MatterCarrier c hc ⟨E⟩
  have hcost : PositiveScaleGroundState ψ ⟨c, hc⟩ :=
    (loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology Eground).2 hground
  refine ⟨⟨c, hc⟩, hcost, ?_⟩
  intro c' hcost'
  obtain ⟨Eground'⟩ := scalePattern_q3MatterCarrier c'.1 c'.property ⟨E⟩
  have hground' : LoadNormalizedToTopology (scalePattern c'.1 ψ) :=
    (loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology Eground').1 hcost'
  apply Subtype.ext
  exact (unique_scale_loadNormalizedToTopology
    (ψ := ψ) (c := c) (c' := c'.1) E hc c'.property hground hground').symm
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
THEOREM gapOne_rhatQuotient_ne_gapTwo · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean
gapOne_rhatQuotient_ne_gapTwo · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean:256 
/-- The two neutral modes determine different points of the named Rhat shape
quotient. -/
theorem gapOne_rhatQuotient_ne_gapTwo :
    Quotient.mk rhatOrbitSetoid gapOneTwoPhaseMode ≠
      Quotient.mk rhatOrbitSetoid gapTwoTwoPhaseMode := by
  intro h
  exact gapOne_not_rhatOrbitEquivalent_gapTwo (Quotient.exact h)

What this page does not claim

The raw T10 uniqueness target is not proved; it is refuted. Pattern uniqueness does not hold on the current Q3 carrier modulo the named physical quotient. The derivation of the anchor mode and topology restriction is not supplied by this module.

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