Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientExamples

show as:
view Lean formalization →

Toy phase-state examples that exercise the phase-quotient construction from QuotientSelection. Supplies a concrete PhaseState type, an empty observable quotient, a separating gauge-family injectivity check, and a projective display map. Downstream delta-native analysis and strong-closure modules import these fixtures. Content is definitional and example-driven rather than a deep proof development.

claimA toy phase-state space $P$ with an observable phase quotient $P/\sim_{\mathrm{obs}}$, a separating family of gauge functionals that injects into the quotient, and a projective display map sending states to their observable classes. Includes the empty-observable edge case where the quotient collapses appropriately.

background

Primitive Recognition Calculus treats recognition events as the primitive ontology. Phase structure appears once one quotients raw states by gauge-equivalent observables: two states are identified when every admissible observable returns the same value.

QuotientSelection supplies the general selection and quotient machinery. This module instantiates that machinery with deliberately small toy phase states so later analytic modules can compute defects, deltas, and closure properties without carrying full physical state spaces.

Sibling objects include a PhaseState carrier, the empty-observable quotient (all states identified when no observable separates them), a lemma that a separating gauge family yields an injective map into the quotient, and a projective display of states by their observable class.

proof idea

Definition and example module, not a single theorem chain. It introduces the PhaseState carrier and builds the empty-observable quotient as a direct instance of the upstream selection quotient. Separating-gauge injectivity is a short algebraic check: if the family separates points, the induced map on the quotient is injective. The projective display is the canonical projection. A headline declaration packages the example suite for importers.

why it matters in Recognition Science

Feeds DeltaNativeAnalysis and DeltaNativeStrongClosure, which import the module to obtain concrete phase-quotient fixtures when analyzing native delta quantities and proving strong closure. In the Recognition foundation layer this sits under Primitive Recognition Calculus: phase quotients are the bridge from raw recognition events to gauge-invariant observables before cost functionals (J-cost, defect distances) and the forcing chain (T5 J-uniqueness onward) are applied. The toys keep those later arguments free of unnecessary state-space bulk while still exercising empty and separating cases.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)