Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCOnePrimitive

show as:
view Lean formalization →

Module for the one-primitive claim in Primitive Recognition Calculus: a distinction has exactly two endpoints, and the atomic act is a same/diff judgment on those endpoints. Comparison is shown to be derived, not primitive. Downstream certificate modules import it to shrink the primitive basis. The content is a short cluster of endpoint and act-judgment lemmas over the Basic and SameDiff layers.

claimA distinction has exactly two endpoints. The atomic recognition act is a judgment that those endpoints are the same or different; genuine sameness coincides with equality. Comparison is a derived notion, not an independent primitive.

background

Primitive Recognition Calculus (PRC) is the foundation layer that isolates what must be taken as primitive before the forcing chain (T0–T8) and the Recognition Composition Law. The Basic import supplies the raw distinction and endpoint vocabulary; SameDiff supplies the same/diff judgment language.

This module tightens that language to a single primitive. The module doc states the core fact: a distinction has exactly two endpoints. Sibling material then defines the act of judgment on a distinction (same versus different), proves that a genuine same-judgment is equality of endpoints, and records that comparison is derived from that act rather than postulated separately.

The setting is purely structural: no metric, no J-cost, and no ladder yet. The goal is to fix the combinatorial skeleton of recognition before cost and self-similarity are forced.

proof idea

Not a single theorem: a small definition-and-lemma module. Endpoint lemmas establish that an endpoint of a distinction is left or right (exhaustive two-point structure). Act-judgment definitions package same and diff as the two possible outcomes of recognizing a distinction, with decidability for the same case. A genuineness lemma identifies a successful same-judgment with endpoint equality. A closing lemma records that comparison is obtained from these acts and is therefore not an extra primitive. Imports from Basic and SameDiff supply the underlying types and same/diff predicates; no deep tactic proof is required beyond case analysis on the two endpoints and the two judgment outcomes.

why it matters in Recognition Science

Recognition Science aims to derive physics from one functional equation and a minimal recognition ontology. This module pins the ontology side: one primitive act (same/diff on a two-endpoint distinction), so later cost, $\phi$, eight-tick structure, and $D=3$ are not smuggling extra primitives.

It is imported by PRCShrunkCertificate, which packages the reduced primitive basis for the rest of the foundation stack. Without the two-endpoint and derived-comparison facts, the certificate cannot claim that the calculus is truly one-primitive. The module does not itself touch T5–T8 or the RCL; it only clears the ground those steps stand on.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)