Primitive
plain-language theorem explainer
Two-constructor inductive naming the starting data of maximal forcing: bare object-level distinction on the bridge carrier, and a Law-of-Logic realization once the floor is non-vacuous. Downstream forcing and ledger-factorization modules cite it as the seed type rather than equating the two notions up front. No proof body: pure datatype with DecidableEq and Repr.
Claim. An inductive type with two constructors: (i) distinction, the object-level claim that there exist $x,y$ in the dimensionless bridge carrier with $x \neq y$; (ii) law-of-logic, a Law-of-Logic realization after the recognition floor is non-vacuous. The constructors remain formally distinct so equivalence can be proved later rather than assumed.
background
This module opens the Maximal Forcing Closure program. The stated target is to start from distinction and the Law of Logic, derive every invariant shared by all admissible realizations, and classify residual degrees of freedom as either forced by a deeper admissibility condition or independent by countermodel. The file only installs the primitive and claim language; it does not assert the crown theorem.
The first constructor is object-level non-triviality on the bridge carrier $K$ (the dimensionless ratio $K=\varphi^{1/2}$ in RS-native units). The second is a Law-of-Logic realization once that floor is non-vacuous. Sibling claim language in the same file (reality claims, forced/independent tags, selection principles) builds on this seed.
Keeping the constructors separate is deliberate: later modules are meant to prove their equivalence rather than silently identify them, so the forcing chain can track which route supplies each invariant.
proof idea
No proof. The declaration is an inductive datatype with two nullary constructors, deriving DecidableEq and Repr. Mathematical content lives entirely in the constructor docs and in downstream theorems that pattern-match on the type.
why it matters
This is the seed type for the Maximal Forcing program: every later claim about what is forced versus independent is indexed against these two primitives. Downstream, ledger-to-factorization results (discrete ledger posting semantics, factorization gates from primitive ledger posting under continuity, monotonicity, or directional regularity) treat primitive posting as the finite, non-completed starting point that forces affine response and the factorization associativity gate. That gate is the bridge from discrete recognition bookkeeping toward the Recognition Composition Law structure used in the broader forcing chain (T5 J-uniqueness onward).
The module doc is explicit that the crown theorem is not asserted here. The datatype only fixes the vocabulary so equivalence of distinction and Law-of-Logic, and the full invariant census, can be stated without circular identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.