Masses Mass Genesis T10 Settled Readout Decision Settled Readout Underdetermined

The underdetermination result

The declaration settledReadout_underdetermined_by_currentBoundary is a theorem in the Recognition Science framework's machine-checked library of formal theorems. In plain language, it proves that the information available at a physical boundary, as currently modeled, is not enough to force a unique answer to a specific question: whether a photon's readout window has the settled-anchor shape. The theorem states this as a formal negation: it is not true that every model of the physical photon and pattern product satisfies the property PhotonWindowIsSettledAnchor.

This is not a statement of ignorance. It is a precise, proved limit on what the current physical boundary data can determine. The theorem is accompanied by a second, stronger result: an explicit countermodel. This is a concrete, kernel-checked example of a model that is compatible with the physical photon and pattern data, where the photon reads the pattern anchor, yet the window is not a settled anchor. The existence of this countermodel is what makes the underdetermination real rather than hypothetical.

The framework's library does not stop at the negative result. It also proves what happens when the missing premise is supplied. A separate theorem, settledReadout_of_settledBoundary, shows that once the boundary is a settled boundary, carrying the settled-anchor field, the photon window is indeed the settled anchor. The underdetermination theorem therefore establishes a precise boundary: the identification of the physical readout with the settled anchor is not derived from bare physical data. It is carried as a named premise, parallel to other carried inputs in the framework's forced-matter closure.

The practical consequence is a clear division of labor. The framework proves that the settled-readout identification is independent of the current physical photon and pattern product, in the sense that no amount of that data alone forces it. It also proves that once the settled boundary is assumed, the identification follows and the mass law, absolute size, and photon energy share all discharge. What the theorem does not claim is that the identification is false, or that it is unprovable in principle. It claims only that the current boundary data are insufficient, and that a specific carried premise is required.

/-- 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

What this page does not claim

The theorem does not claim that the settled-readout identification is false. The theorem does not claim that the identification is unprovable in principle from some other data. The theorem does not claim that the current boundary data are irrelevant; it claims only that they are insufficient.

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: