forcedOne
plain-language theorem explainer
Defines the forced multiplicative unit on a Law-of-Logic realization: the image of the natural-number one under the inverse orbit equivalence to the reference initial object. Anyone proving that the canonical Peano (or ordered-semiring) isomorphism preserves units cites this constant. The body is a one-line transport of 1 along that equivalence.
Claim. For any Law-of-Logic realization $R$, the forced unit on the Peano carrier of its forced arithmetic is the pullback of $1 \in \mathrm{LogicNat}$ along the inverse of the orbit equivalence $R \simeq \mathrm{LogicNat}$.
background
Universal Forcing Part II upgrades the bare carrier bijection of Part I to a structure-preserving map of Peano algebras, then further to the arithmetic those Peano data determine: constants $0$ and $1$, addition, multiplication, and order. The reference initial object is $\mathrm{LogicNat}$, the two-constructor type with identity (zero-cost element) and step (generator iteration), recovered as the orbit ${1,\gamma,\gamma^2,\ldots}$.
A Law-of-Logic realization supplies a carrier, comparison cost, identity, and step action. Its forced arithmetic is the Peano algebra extracted from that identity/step data. Every such forced carrier folds canonically onto $\mathrm{LogicNat}$ by the orbit equivalence; arithmetic on the forced carrier is defined by transporting the already-proved arithmetic on $\mathrm{LogicNat}$ along that fold.
This declaration is the unit half of that transport (the zero half is the sibling forced-zero constant). The load-bearing compatibility fact later is that the universal forcing isomorphism composed with one realization's fold equals the other's fold, by initiality of Peano homomorphisms into $\mathrm{LogicNat}$.
proof idea
Pure definitional transport: apply the inverse of the realization's orbit equivalence $\mathrm{LogicNat}\to$ forced Peano carrier to the numeral $1$ on $\mathrm{LogicNat}$. No tactic proof; the term is exactly that inverse image. Downstream lemmas then rewrite with fold-iso compatibility and Equiv.apply_symm_apply to show the canonical map sends this unit to the unit of any other realization.
why it matters
Closes the constant-$1$ slot in the ordered-semiring layer of Universal Forcing. The certificate structure for ordered-semiring isomorphism requires that the canonical Peano equivalence send forced unit to forced unit for every pair of realizations; the companion theorem that states exactly that preservation is a one-line injectivity-plus-simp argument built on this definition and fold-iso compatibility.
Together with the forced-zero, forced-add, forced-mul, and forced-order transports, this supplies the element-level content of an ordered commutative semiring isomorphism across all Law-of-Logic realizations, without needing a Mathlib OrderedCommSemiring instance on the carriers. It sits downstream of the Peano-algebra uniqueness already established in the canonical-iso module and upstream of the bundled certificate that packages zero, one, add, mul, and order preservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.