Masses Mass Genesis T10 Settled Readout Decision

The settled readout decision

In the Recognition Science framework, recognition events are the discrete record of what exists. The T10 settled-readout decision is the step where the framework asks whether the physical photon readout, the pattern of energy a photon carries after interacting with matter, is the same as the settled anchor shape that the theory's own laws have already derived. The settlement shape is not in question; it follows from the commit-settlement law. The open question is whether nature's photon readout actually is that shape.

The module proves that the current physical boundary data, the information available from the photon and pattern models, do not by themselves determine the settlement shape. A kernel-checked theorem, settledReadout_underdetermined_by_currentBoundary, shows that not every physical-photon-compatible model has a photon window that is a settled anchor. A second theorem, settledReadout_gapTwo_countermodel, exhibits an explicit countermodel: a physical-photon-compatible Q3 carrier where the photon reads the pattern anchor but is not a settled anchor. These two results establish that the identification is not forced by the bare physical data.

The decision, called Branch C, is to carry the settled-readout identification as a named premise on the physical boundary interface. Once that interface is carried, the identification discharges: a theorem proves that on the settled boundary, the photon window is the settled anchor. This is the final form for this rung. The module is explicit that deriving this identification from bare posting, photon, and Q3 data remains outside the closed claim; that wall stands.

With the carried interface, the forced-matter closure completes. The module proves a mass law: rest mass equals predicted mass. It proves absolute size: posting amplitude squared equals predictedMass divided by 16. It proves the photon mass share: the eight-tick window energy equals predictedMass divided by 8. It proves uniqueness: same-topology forced matter is unique in both pattern and amplitude. And it proves non-vacuity: the three-input interface is inhabited. The certificate theorem, t10SettledReadoutDecisionCert, packages all of these results into a single settled-readout decision.

What this establishes in plain language is that the framework's mass law is not a free choice. Given the settled boundary and the sigma-zero constraint, the mass, the amplitude, and the photon's share are all forced. The price is honesty: the readout identification itself is carried, not derived. The module names its three inputs: the settled current physical boundary, the RS sigma-zero constraint, and the carried Branch-C readout identification. Origin is already Branch-B relative to the carried indexing. The framework does not claim more than its premises allow, and the T10 module is the record of exactly what those premises are.

/-- Current physical boundary data underdetermine settlement shape. -/
theorem settledReadout_underdetermined_by_currentBoundary :
    ¬ ∀ model : PhasePostingPhysicalPhotonQ3Model3,
      PhotonWindowIsSettledAnchor model.photon model.pattern :=
  currentPhysicalBoundary_does_not_force_settledAnchorWindow

/-- Explicit gap-two countermodel: Q3 carrier, physical-photon compatible,
photon reads pattern anchor, yet not a settled anchor. -/
theorem settledReadout_gapTwo_countermodel :
    ∃ model : PhasePostingPhysicalPhotonQ3Model3,
      ¬ PhotonWindowIsSettledAnchor model.photon model.pattern :=
  exists_physicalBoundary_not_settledAnchor

/-- On the settled boundary interface the photon window IS the settled
anchor (by the carried field). -/
theorem settledReadout_of_settledBoundary
    (model : SettledCurrentPhysicalBoundaryModel3) :
    PhotonWindowIsSettledAnchor
      model.base.photon model.base.pattern :=
  PhotonWindowIsSettledAnchor.ofSettledBoundary model

/-- Mass law on the physical boundary. -/
theorem restMass_eq_predictedMass
    (iface : ForcedMatterInterface3) :
    restMass iface.model.boundary.base.pattern =
      predictedMass iface.model.boundary.base.pattern :=
  iface.model.restMass_eq_predictedMass

/-- Absolute size: posting amplitude squared equals predictedMass/16. -/
theorem absolute_size
    (iface : ForcedMatterInterface3) :
    iface.model.boundary.amplitude ^ 2 =
      predictedMass iface.model.boundary.base.pattern / 16 :=
  iface.model.amplitude_sq_eq_predictedMass_div_sixteen

/-- Same-topology forced matter is unique in pattern. -/
theorem sameTopology_pattern_unique
    (left right : ForcedMatterInterface3)
    (htop :
      left.model.boundary.base.pattern.topology =
        right.model.boundary.base.pattern.topology) :
    left.model.boundary.base.pattern =
      right.model.boundary.base.pattern :=
  physicalSettledSigmaZero_sameTopology_pattern_unique
    left.model right.model htop

/-- Same-topology forced matter is unique in posting amplitude. -/
theorem sameTopology_amplitude_unique
    (left right : ForcedMatterInterface3)
    (htop :
      left.model.boundary.base.pattern.topology =
        right.model.boundary.base.pattern.topology) :
    left.model.boundary.amplitude = right.model.boundary.amplitude :=
  physicalSettledSigmaZero_sameTopology_amplitude_unique
    left.model right.model htop

What this page does not claim

The settled-readout identification is derived from the bare physical data; it is carried as a named premise. The mass law applies without the settled boundary interface and the sigma-zero constraint. The T10 module proves the physical recognition-to-linking bridge that connects recognition events to spatial topology.

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