Masses Mass Genesis T10 Sigma Zero Forced Matter Physical Settled Sigma Zero Sam

A unique size for matter

In physics, a particle's mass fixes its energy and its gravity, but the absolute size of the thing that carries that mass is a separate question. Two particles could have the same mass and different radii. Recognition Science asks whether its own framework can pin that size down. The answer, for settled matter, is yes: a machine-checked theorem in its library proves that particles with the same internal topology must post the same amplitude, which is the framework's word for size.

The theorem is physicalSettledSigmaZero_sameTopology_amplitude_unique, and it is conditional. It assumes a model of the physical boundary that includes the sigma-zero field, the framework's single named physical constraint, which sets the cost of recognition to zero. Given that field, the theorem proves that any two settled matter patterns with the same topology have the same posting amplitude. The proof chains through the mass law, which equates rest mass to predicted mass, and the amplitude equation, which ties the posting amplitude to the primitive factor amplitude selected by the topology. Since the topology is the same, the selected amplitude is the same.

What this does not claim is that the sigma-zero field itself is forced by the settled boundary data. The walls proving that current boundary data do not force sigma-zero remain in force. The theorem also does not claim that different topologies have different amplitudes, nor does it give a numerical value for any particle's mass. It establishes uniqueness within a topology, not a spectrum across topologies.

/-- Same-topology sigma-zero matter also posts at the same amplitude. -/
theorem physicalSettledSigmaZero_sameTopology_amplitude_unique
    (left right : PhysicalSettledSigmaZeroModel3)
    (htop :
      left.boundary.base.pattern.topology =
        right.boundary.base.pattern.topology) :
    left.boundary.amplitude = right.boundary.amplitude := by
  have hpat :=
    physicalSettledSigmaZero_sameTopology_pattern_unique left right htop
  rw [left.amplitude_eq_primitiveFactorAmplitude,
    right.amplitude_eq_primitiveFactorAmplitude, hpat]

What this page does not claim

The sigma-zero field is forced by the settled boundary data. Different topologies have different posting amplitudes. Any specific particle mass is numerically derived in this theorem.

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