Generator
plain-language theorem explainer
A Generator packages any positive real number other than 1 as the base for embedding LogicNat into the positive reals. Researchers deriving arithmetic from the laws of logic cite this structure as the witness supplied by the non_trivial field of SatisfiesLawsOfLogic. The declaration is a bare structure definition that records the positivity and nontriviality conditions.
Claim. A generator is a real number $γ$ satisfying $γ > 0$ and $γ ≠ 1$.
background
In ArithmeticFromLogic the derivation of natural-number arithmetic begins from a comparison operator that obeys the laws of logic. SatisfiesLawsOfLogic (from LogicAsFunctionalEquation) is the structure requiring identity, non-contradiction, excluded middle, scale invariance and route independence, together with a non_trivial field that guarantees a positive real distinct from 1. The Generator structure extracts that witness and supplies it to the orbit-embedding constructions that follow.
proof idea
The declaration is a structure definition; it directly records the three fields value, pos and nontrivial with no further lemmas or tactics applied.
why it matters
Generator supplies the parameter to embed, embed_add, embed_eq_pow and the monotonicity theorems that realize LogicNat as the orbit {1, γ, γ², …}. It therefore closes the structural step from SatisfiesLawsOfLogic to concrete arithmetic inside the Recognition framework. The construction is cited by the chain-closure comment as the point at which the abstract logic laws become an explicit multiplicative generator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.