Masses Mass Genesis T10 Physical Sigma Zero Selection Physical Settled Sigma Zer

The uniqueness theorem

The declaration physicalSettledSigmaZero_sameTopology_pattern_unique is a theorem in the framework's machine-checked library of formal theorems. It states that if two complete physical models both carry a matter pattern at zero load-recognition cost, and if those two patterns share the same topology, then the two patterns are identical. In plain terms: within the framework, for a given topology, there is at most one matter pattern that satisfies the zero-cost physical condition. The theorem does not say that such a pattern exists; it says that if two exist, they are the same.

To see what this means, consider the framework's vocabulary. A ledger, a discrete record of recognition events, assigns a cost, a forced price, to each pattern. The theorem concerns models where this cost is exactly zero for the matter pattern itself. The framework proves that this zero-cost condition, together with the topology, uniquely determines the pattern. The result is a rigidity statement: the physical condition, when it holds, leaves no freedom in the pattern's shape.

The theorem is one piece of a larger story about mass genesis in the framework. The framework models a physical boundary that includes a photon and a matter pattern. A separate theorem, exists_settledCurrentPhysicalBoundary_photonZero_patternNonzero, shows that the current boundary conditions do not force the pattern's load cost to be zero. The photon's propagating mode can have zero cost while the pattern does not. The uniqueness theorem applies only after the missing condition, the pattern's zero load cost, is added as an explicit premise.

The framework also proves that this zero-cost condition is consistent: there exists at least one model satisfying it. This non-vacuity result, physicalSettledSigmaZeroModel_nonempty, shows the condition is not contradictory. But consistency is not selection. The framework does not prove that the actual physical boundary must satisfy the zero-cost condition. That selection remains an open premise, a target for future derivation.

What the theorem changes is the shape of the remaining problem. The framework has reduced the task of determining the matter pattern to a single missing step: showing that the physical boundary selects the zero-cost representative. Once that step is supplied, the uniqueness theorem guarantees the pattern is fixed by topology alone. The theorem does not provide the selection law; it sharpens what the selection law would achieve.

/-- Two physically selected settled sigma-zero models with the same topology
carry the same Q3 matter pattern.  This is the full per-topology rigidity
consequence of the missing physical selection field. -/
theorem physicalSettledSigmaZero_sameTopology_pattern_unique
    (left right : PhysicalSettledSigmaZeroModel3)
    (htop :
      left.boundary.base.pattern.topology =
        right.boundary.base.pattern.topology) :
    left.boundary.base.pattern = right.boundary.base.pattern := by
  obtain ⟨Eleft⟩ := left.boundary.base.q3_carrier
  obtain ⟨Eright⟩ := right.boundary.base.q3_carrier
  exact q3Pattern_unique_of_sameTopology_settledAnchor
    Eleft Eright htop
    left.boundary.settled_anchor right.boundary.settled_anchor
    left.amplitude_eq_factorAmplitude
    right.amplitude_eq_factorAmplitude

/-- **Physical boundary wall.** The current settled physical boundary class
does not force the matter pattern to be the sigma-zero representative. -/
theorem currentSettledPhysicalBoundary_does_not_force_patternSigmaZero :
    ¬ ∀ model : SettledCurrentPhysicalBoundaryModel3,
      loadRecognitionCost model.base.pattern = 0 := by
  intro hall
  obtain ⟨model, _hphoton, hpattern⟩ :=
    exists_settledCurrentPhysicalBoundary_photonZero_patternNonzero
  exact hpattern (hall model)

/-- The sigma-zero-enriched physical interface is consistent and inhabited.
A positive scale of the unit settled gap-one worldline supplies a witness.
This proves non-vacuity, not selection of that witness by current boundary
data. -/
theorem physicalSettledSigmaZeroModel_nonempty :
    Nonempty PhysicalSettledSigmaZeroModel3 := by
  obtain ⟨Eseed⟩ := q3MatterCarrier_worldlinePattern_gapOne
  obtain ⟨c, hc, hload⟩ :=
    exists_scale_loadNormalizedToTopology Eseed
  let ψ :=
    scalePattern c (worldlinePattern gapOneTwoPhaseMode)
  have Eψ : Q3ClosedPatternEvidence ψ :=
    scalePattern_q3ClosedEvidence c hc Eseed
  have hcarrier : Q3MatterCarrier ψ := ⟨Eψ⟩
  have hunit :
      SettledAnchorWindow 1 (worldlinePattern gapOneTwoPhaseMode) := by
    unfold SettledAnchorWindow
    funext t
    simp [worldlinePattern, commitSettlementWindow_zero_eq_gapOne]
  have hwin : SettledAnchorWindow c ψ := by
    simpa [ψ] using scalePattern_settledAnchor c hunit
  have hcost : loadRecognitionCost ψ = 0 := by
    exact (loadRecognitionCost_eq_zero_iff_loadNormalizedToTopology Eψ).2
      hload
  exact ⟨
    { boundary :=
        settledCurrentPhysicalBoundaryModelOf hc hcarrier hwin
      pattern_sigma_zero := hcost }⟩

What this page does not claim

The theorem does not prove that the zero-cost condition actually holds for the physical boundary. The theorem does not establish that a sigma-zero pattern exists for every topology. The theorem does not identify which topology corresponds to any particular particle mass.

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/T10PhysicalSigmaZeroSelection.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: