Encyclopedia Masses Masses Mass Genesis T10 Uniqueness Q3 Pattern Unique Of Same Topology Raw Canoni

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Uniqueness Q3 Pattern Unique Of Same Topology Raw Canoni

A machine-checked theorem proves that once a specific anchor mode is fixed, a particle's pattern is unique; the theorem does not prove that the anchor itself is forced.

Verify this page

The shape-selection wall

The declaration q3Pattern_unique_of_sameTopology_rawCanonicalPositiveStationary is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states a conditional uniqueness result: if two light patterns share the same topology, and both satisfy the specific anchor condition called raw canonical positive-stationary primitive factor mode, then the two patterns are identical. In plain language, once you fix the topology and the anchor mode, the entire pattern is determined; there is no second distinct pattern with those same properties.

This theorem is one piece of a larger target called T10, which aims to prove that matter patterns are unique. The framework's own documentation is explicit that the raw version of this target, which quantifies over every stable closed light pattern, is false on the present carrier. Stability alone, defined as locality plus positive neutral load, admits a second stable pattern. The theorem here narrows the claim: it does not say uniqueness holds for all stable patterns, only for those that also satisfy the anchor condition and share a topology.

The proof relies on a simpler lemma: for two patterns with the same topology and the same anchor condition, their first windows are equal. The full theorem extends this equality to the whole pattern. The framework also proves that each of two distinct gap modes, gap-one and gap-two, reaches a unique positive ground-state scale under the cost function, and that these two modes lie in different quotient classes under the phase-gap cost. This shows the uniqueness result is sharp: without the anchor condition, distinct patterns with distinct ground states exist.

What the theorem does not claim is that the anchor mode itself is derived. The framework states plainly that deriving the anchor mode and the topology restriction remains open. The theorem supplies rigidity after these are given, not the physical mechanism that selects them. The missing physics is the derivation of the anchor mode, not the rigidity that follows from it.

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 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 · exists_distinct_gapGroundStates · 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
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 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 theorem does not prove that the anchor mode itself is forced or derived. The theorem does not prove uniqueness for all stable patterns, only for those satisfying the anchor condition. The theorem does not identify which gap mode, if either, corresponds to a physical particle.

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