StrictLogicRealization
plain-language theorem explainer
StrictLogicRealization equips a carrier type with a symmetric cost function to a zero-cost type, a binary composition, distinguished elements one and generator, and propositional laws for identity, symmetry, excluded middle, composition, invariance, plus generator non-triviality. Researchers on the Recognition Science universal forcing path cite it to guarantee that the free orbit is always derived as the LogicNat iteration object rather than carried internally. The declaration is a pure structure with zero proof body.
Claim. A strict logic realization consists of a carrier set $C$, a cost set $K$ with zero element, a comparison $d:C×C→K$, a composition operation $∘:C×C→C$, elements $1,γ∈C$, such that $d(x,x)=0$ for all $x∈C$, $d(x,y)=d(y,x)$ for all $x,y∈C$, the propositions for excluded middle, composition law and invariance law hold, and $d(γ,1)≠0$.
background
The StrictRealization module removes the internal orbit field present in the earlier LogicRealization interface so that the free orbit used by universal forcing is derived uniformly as LogicNat. LogicNat is the inductive type whose constructors identity (zero-cost multiplicative identity) and step (one generator iteration) generate the smallest subset of positive reals closed under multiplication by the generator and containing 1. The local theoretical setting is the domain-rich Universal Forcing interface whose goal is to prove the lightweight universal forcing theorem from native law data only.
proof idea
This is a structure definition with no proof body. The fields directly record the carrier, cost, zero instance, comparison, composition, one, generator, and the six laws (four as propositions). The zeroCost field is registered as an instance via the attribute declaration.
why it matters
StrictLogicRealization supplies the base type for AdmissibleRealization and AdmissibleClassCert in the AdmissibleClass module; those structures add decidability of cost equality and associativity of composition. It feeds the quantified_universal_forcing theorem, which asserts that the universal forcing equivalence is available for any pair of admissible strict realizations. In the Recognition Science framework it closes the path from the Law of Logic to the natural-number object without internal orbit assumptions, aligning with the forcing chain that derives LogicNat and ultimately D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.