Encyclopedia Masses Masses Mass Genesis T10 Uniqueness Primitive Positive Stationary Factor Amplitud

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Uniqueness Primitive Positive Stationary Factor Amplitud

A machine-checked theorem shows that once a mass pattern's topology is fixed, its primitive stationary factor amplitude is fixed too, but full pattern uniqueness remains open.

Verify this page

Scale rigidity

In the Recognition Science framework, mass patterns are represented as discrete light patterns on an eight-tick cycle, and each pattern carries a topology that encodes how its primitive sectors are arranged. The theorem primitivePositiveStationaryFactorAmplitude_eq_of_sameTopology states that if two such patterns have the same topology, then their primitive positive stationary factor amplitudes are equal. This is a machine-checked theorem in the framework's library of formal theorems, meaning the equality is derived from the definitions by a proof checker, not assumed.

The amplitude in question is the primitive factor amplitude, a number extracted from the pattern's anchor sector that plays a role in mass scaling. The theorem says this number depends only on the topology, not on the other details of the pattern. This is a scale rigidity result: at fixed topology, the amplitude is rigid. The proof is short: it unfolds the definitions of the amplitude, the sector load, the primitive transport, and the sector and rung functions, then rewrites the topology equality. The equality is derived in the framework and checked in the library.

The theorem does not claim that whole patterns are unique. In fact, the raw uniqueness target, which would say every stable closed light pattern is unique, is false on the current carrier. There are at least two distinct stable patterns, the gap-one mode and the gap-two mode, each with its own positive ground-state scale. The theorem also does not claim that the amplitude itself is derived from first principles; it is defined, not derived. The physical derivation of the anchor mode and the topology restriction remains open.

What the theorem does establish is a conditional rigidity: once the topology is fixed and the pattern is in the canonical positive stationary primitive factor mode, the entire pattern is determined. This is a sharp result, but it depends on the mode being supplied. The missing physics is the derivation of that mode and the topology restriction, not the rigidity after they are supplied.

THEOREM primitivePositiveStationaryFactorAmplitude_eq_of_sameTopology · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean
primitivePositiveStationaryFactorAmplitude_eq_of_sameTopology · IndisputableMonolith/Masses/MassGenesis/T10Uniqueness.lean:86 
/-- The canonical positive-stationary amplitude reads only topology. -/
theorem primitivePositiveStationaryFactorAmplitude_eq_of_sameTopology
    {ψ χ : LightPattern (Fin 8)} (htop : ψ.topology = χ.topology) :
    primitivePositiveStationaryFactorAmplitude ψ =
      primitivePositiveStationaryFactorAmplitude χ := by
  unfold primitivePositiveStationaryFactorAmplitude
  unfold primitiveAnchorSectorLoad primitivePhiTransport
  unfold sectorOf rungOf ZOf
  rw [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 claim that whole light patterns are unique; the raw uniqueness target is false. The theorem does not claim that the primitive factor amplitude is derived from first principles; it is defined. The theorem does not claim that the gap-one and gap-two modes are physically equivalent; they lie in different Rhat quotient classes.

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