Generator
plain-language theorem explainer
Generator is a structure for any positive real γ ≠ 1 that parameterizes the orbit embedding of LogicNat into ℝ₊. Researchers deriving arithmetic operations from the functional equation of logic cite it to instantiate the base of iteration. The definition is a direct structural extraction from the non_trivial field of SatisfiesLawsOfLogic together with the identity lemma.
Claim. A generator is a real number $γ > 0$ satisfying $γ ≠ 1$.
background
In the ArithmeticFromLogic module the construction of natural-number arithmetic begins from SatisfiesLawsOfLogic, the structure asserting that a comparison operator obeys identity, non-contradiction, excluded middle, scale invariance and route independence. The upstream result SatisfiesLawsOfLogic.non_trivial supplies a witness that the derived cost function is not identically zero. Generator packages that witness as a positive real distinct from the identity element 1, which is the fixed point of the J-cost minimum.
proof idea
The declaration is a structure definition whose three fields are value : ℝ, pos : 0 < value and nontrivial : value ≠ 1. No tactics or lemmas are applied; the fields are taken verbatim from the non_trivial component of SatisfiesLawsOfLogic and the identity event.
why it matters
Generator supplies the parameter for the downstream embed, embed_add, embed_eq_pow and embed_injective theorems that realize LogicNat as the orbit {1, γ, γ², …}. It therefore closes the passage from the abstract SatisfiesLawsOfLogic to concrete multiplicative arithmetic inside the Recognition framework. The construction is the explicit structural completion of the chain that begins with the Law of Logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.