toLightweight
plain-language theorem explainer
The definition converts a strict logic realization R, supplying only native comparison, composition, and law data without an internal orbit, into the lightweight LogicRealization interface by deriving the orbit uniformly from LogicNat. Researchers auditing domain realizations in biology, ethics, music, and categorical structures cite it to obtain the arithmetic equivalence to LogicNat. The construction is a direct field-by-field mapping that sets orbit operations to LogicNat constructors and proves interpret and orbit steps by reflexivity.
Claim. Let $R$ be a strict logic realization. Then toLightweight$(R)$ is the logic realization whose carrier is $R$.Carrier, cost type is $R$.Cost with zero $R$.zeroCost, comparison is $R$.compare, zero element is $R$.one, successor step is $x mapsto R$.compose$(R$.generator$, x)$, orbit is FreeOrbit$(R)$, orbit zero and step are LogicNat.identity and LogicNat.succ, interpretations are given by interpret$(R)$, and all laws (identity, non-contradiction, excluded middle, composition, invariance, nontriviality) are taken directly from the corresponding fields of $R$.
background
A strict logic realization is a structure carrying a carrier type, a cost type equipped with zero, a comparison map from carrier pairs to cost, a binary composition, distinguished elements one and generator, and laws asserting that compare is an identity (zero on diagonals), symmetric under swap, satisfies non-contradiction, excluded middle, composition, invariance under action, and nontriviality via the generator. The module StrictRealization derives the free orbit for universal forcing as the inductive type LogicNat whose constructors identity and step mirror the orbit generated by repeated multiplication by the generator starting from one. Upstream, LogicNat is introduced as the smallest subset of positive reals closed under multiplication by the generator and containing one; its successor is shown injective by constructor disjointness, and induction is available as a theorem of the inductive structure. The local setting removes the internal orbit field that the earlier lightweight interface permitted, forcing every realization to use the uniform LogicNat derivation.
proof idea
The definition constructs the target LogicRealization record by direct assignment of carrier, cost, zeroCost, compare, one, and the law fields from the input R. The orbit is set to FreeOrbit R with zero and step taken from LogicNat.zero and LogicNat.succ. The interpret field is supplied by the sibling interpret function on R; interpret_zero and interpret_step are proved by reflexivity. Orbit no-confusion uses LogicNat.zero_ne_succ, orbit step injectivity uses LogicNat.succ_injective, and orbit induction uses LogicNat.induction. The orbit equivalence to LogicNat is reflexivity, and the remaining laws are referenced verbatim from the corresponding fields of R.
why it matters
This definition supplies the uniform bridge from the strict interface (native laws only) to the lightweight interface whose orbit already satisfies the forcing chain, enabling the strict path through the universal forcing theorem. It is invoked in the AxiomAudit module to establish that each domain realization (strictBiologyRealization, strictCategoricalRealization, strictEthicsRealization, strictMusicRealization, strictNarrativeRealization, strictOrderedRealization) yields an arithmetic carrier equivalent to LogicNat via the orbitEquivLogicNat field. The conversion closes the gap between supplied law data and derived Peano structure, supporting the claim that strict realizations realize the same arithmetic without ad-hoc orbits. It touches the open question of whether every domain realization satisfies the full set of forcing laws uniformly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.