normalized_floor_to_positive_ratio_arithmetic
plain-language theorem explainer
The Boolean normalized recognition floor and any continuous positive-ratio comparison obeying the laws of logic force equivalent Peano arithmetic carriers. Cite this when identifying the arithmetic object shared by the absolute-floor and T0 logic realizations. The proof rewrites both carriers as orbits and composes the two orbit-to-LogicNat equivalences.
Claim. Given a normalized two-point recognition floor on $\mathrm{Bool}$ (unit-normalized recognition-work cost, exhaustive empty/marked split) and a comparison operator $C:\mathbb{R}_{>0}\times\mathbb{R}_{>0}\to\mathbb{R}$ satisfying the laws of logic (identity, non-contradiction, excluded middle, scale invariance, route independence), the Peano carrier of the arithmetic of the floor realization is equivalent to that of the positive-ratio realization of $C$.
background
This lives in the Unified Forcing Chain module, which derives T-1 through T8 from the Recognition Composition Law plus normalization and calibration. T-1 is the absolute floor (meta-language distinction plus a non-singleton universe); T0 is logic forced by cost minimization.
A normalized two-point recognition floor is the abstract Boolean floor: one empty/consistent configuration, one marked inconsistent point, a unit-normalized recognition-work cost, and an equivalence to $\mathrm{Bool}$ so that $\mathrm{Bool}$ is only the canonical representative. A comparison operator is a real-valued cost of comparing two positive quantities; it satisfies the laws of logic when the four Aristotelian constraints hold together with scale invariance and non-triviality.
arithmeticOf supplies, for any logic realization, the canonical initial Peano object. Both the floor realization (from the normalized floor) and the positive-ratio realization (from $C$) therefore carry Peano structure; the claim is that those carriers coincide up to equivalence.
proof idea
One-line transport after a definitional rewrite. Change the goal from Peano-carrier equivalence to orbit equivalence of the two realizations. Apply the floor realization's orbitEquivLogicNat, then compose with the inverse of the positive-ratio realization's orbitEquivLogicNat. Both orbits are identified with the same LogicNat carrier, so the composite is the desired equivalence.
why it matters
Closes the arithmetic-identification step between the absolute-floor (T-1) side and the continuous positive-ratio logic side of the forcing chain. The module's stronger claim is a complete inevitability chain from cost foundation through T0 logic to T5 unique $J$, T6 $\varphi$, T7 eight-tick, and T8 $D=3$. Showing that floor and positive-ratio realizations force the same Peano object means the arithmetic content does not depend on which presentation of logic one starts from.
No downstream consumers are wired yet (used_by is empty), so this is presently a bridge definition inside the chain rather than a cited lemma in later physics extractions. It supports the narrative that T0 arithmetic is realization-invariant once the laws of logic hold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.