IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientExamples
Toy finite phase-state models that illustrate the phase quotient construction from QuotientSelection. Supplies concrete carriers, empty-observable quotients, and a separating gauge family used to check injectivity of the display map. Downstream native-delta analysis imports these examples as sanity checks. Content is definitional and lemma-light: small explicit sets and elementary injectivity arguments.
claimFinite toy phase states $P$, an empty-observable phase quotient, a separating family of gauge functionals whose joint map is injective, and a projective display of states on the quotient. These are worked examples of the abstract phase-quotient selection machinery.
background
In the Primitive Recognition Calculus, physical content is read only through gauge-invariant observables. QuotientSelection packages the abstract phase quotient: identify states that no allowed observable can separate. This module sits one layer down and gives finite, hand-checkable carriers so that the quotient, the display map, and separation can be inspected without the full continuum machinery.
The main named objects are a toy phase-state type, the quotient by the empty observable set (everything collapses), a separating family of gauge maps whose joint evaluation is injective, and a projective display of states on the quotient. The setting is purely kinematic: no dynamics, no mass ladder, and no forcing-chain step is claimed here.
Upstream material is the QuotientSelection import; Mathlib supplies ordinary finite types and injectivity lemmas.
proof idea
Definition module with a few elementary lemmas, not a theorem chain. Phase states are introduced as an explicit finite type. The empty-observable quotient is the universal collapse when no observable is present. Separating-gauge injectivity is a direct check that a listed family of functionals jointly separates points. Projective display packages the quotient projection as a concrete map. A headline declaration aggregates the example for importers. No deep tactic scripts; proofs are definitional equality and finite-case injectivity.
why it matters in Recognition Science
Gives DeltaNativeAnalysis and DeltaNativeStrongClosure a minimal, importable sandbox for phase-quotient bookkeeping before native delta estimates are run in earnest. Without a finite example, quotient selection stays abstract and hard to audit. The module does not advance T5–T8 or the Recognition Composition Law; it only stabilizes the kinematic language those later layers assume when they talk about gauge-invariant displays of recognition states. Parent consumers are the two native-delta modules that import it wholesale.
scope and limits
- Does not prove uniqueness of the physical phase quotient beyond the toy carrier.
- Does not derive J-cost, RCL, or any forcing-chain step T5–T8.
- Does not model continuum or Hilbert-space phases; carriers are finite toys.
- Does not assert dynamical stability or measurement postulates.
- Does not close native-delta bounds; those live in downstream modules.