IndisputableMonolith.Foundation.UniversalForcing.ForcedIntegers
Module that embeds forced numbers into the integers by iteration count, yielding a ring homomorphism from the forced semiring. It packages injectivity, nonnegativity, and surjectivity onto Z, plus difference lemmas and a certificate. Anyone citing the forced-integer step of Universal Forcing needs this bridge. Structure is definitional embedding plus elementary algebraic identities.
claimFrom the forced semiring one obtains a map $\mathrm{toInt}$ sending each forced number to the integer equal to its iteration count. The map preserves $0$, $1$, addition and multiplication, is injective, lands in the nonnegative integers on the forced nonnegative cone, and is surjective onto $\mathbb{Z}$. Forced differences satisfy the usual zero, negation-swap, and fixed-point identities.
background
Universal Forcing builds arithmetic structure from Recognition Science constraints rather than assuming $\mathbb{Z}$ a priori. The upstream module ForcedSemiring supplies the forced nonnegative arithmetic (addition, multiplication, zero, one) forced by the same functional equation that yields the J-cost $J(x)=(x+x^{-1})/2-1$ and the golden ratio fixed point.
This module lifts that semiring into the integers by reading off iteration count: each forced number is identified with how many times the generating step has been applied. The resulting embedding is the canonical bridge from forced nonnegative arithmetic to full $\mathbb{Z}$.
Notation: $\mathrm{toInt}$ is the embedding; forced differences are the integer differences of images under $\mathrm{toInt}$. The certificate packages the homomorphism and bijectivity facts for downstream use.
proof idea
Definitional core: $\mathrm{toInt}$ is defined by iteration count on the forced generators. Homomorphism lemmas ($0$, $1$, add, mul) are direct inductions or rewrites from the ForcedSemiring operations. Injectivity and nonnegativity follow from the counting interpretation. Surjectivity onto $\mathbb{Z}$ uses the difference construction (positive and negative directions). The three difference lemmas are elementary identities on those differences. ForcedIntegersCert assembles the package; no deep analytic argument is required.
why it matters in Recognition Science
In the Recognition Science forcing chain, integers cannot be smuggled in as a background set; they must be recovered from the forced semiring. This module is that recovery step inside UniversalForcing. It sits immediately above ForcedSemiring and supplies the integer layer needed for later forcing of rationals, dimensions, and the eight-tick octave structure (T7) and $D=3$ (T8).
No downstream edges are recorded in the graph snapshot, so parent theorems are not named here; the natural consumers are any UniversalForcing results that quantify over $\mathbb{Z}$ or use signed differences of forced quantities. The certificate is the stable interface those results should import.
scope and limits
- Does not construct the forced semiring; that is upstream ForcedSemiring.
- Does not force rationals, reals, or continuum structure.
- Does not prove uniqueness of the embedding up to unique isomorphism beyond injectivity and surjectivity stated here.
- Does not connect to J-cost identities, phi-ladder masses, or physical constants.
- Does not discharge any sorry outside this module's own certificate packaging.
depends on (1)
declarations in this module (13)
-
def
toInt -
theorem
toInt_zero -
theorem
toInt_one -
theorem
toInt_add -
theorem
toInt_mul -
theorem
toInt_injective -
theorem
toInt_nonneg -
theorem
integers_surject -
theorem
forced_difference_zero_iff -
theorem
forced_difference_neg_swap -
theorem
forced_difference_fixed_iff -
structure
ForcedIntegersCert -
def
forcedIntegersCert_holds