ordered_interpret_le_iff
plain-language theorem explainer
The equivalence shows that the partial order on the LogicNat carrier coincides exactly with the standard ordering on natural numbers recovered by counting steps from the identity element. Workers on the ordered realization of the forcing chain cite this when confirming that the inductive carrier preserves the Peano structure without distortion. The proof reduces immediately to the symmetry of the upstream toNat_le theorem.
Claim. For all $a, b$ in the inductive type LogicNat, the inequality toNat$(a) ≤$ toNat$(b)$ holds if and only if $a ≤ b$.
background
LogicNat is the inductive type with constructors identity (the zero-cost element) and step (one iteration of the generator), mirroring the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ and containing 1. The function toNat extracts the iteration count, sending identity to 0 and step n to the successor of toNat n. The upstream theorem toNat_le states that LogicNat carries a partial order equivalent to the order on its image under toNat. This declaration sits in the OrderedLogicRealization module, which supplies an ordered faithful realization for Universal Forcing.
proof idea
The proof is a one-line wrapper that applies the symmetry of the toNat_le lemma from ArithmeticFromLogic.
why it matters
This equivalence ensures the order in the ordered realization matches the recovered Peano order, supporting the faithful embedding required for the forcing chain. It underpins subsequent invariants such as ordered_arithmetic_invariant and ordered_faithful in the same module. No open questions are directly addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.