structure
definition
def or abbrev
back
show as:
view Lean formalization →
formal statement (Lean)
513structure back to the comparison operator that started the chain. The
514embedding `LogicNat → ℝ₊` sends `n` to `γⁿ` for any non-trivial
515generator `γ` of the multiplicative group of positive reals. This is
516the structural witness that the abstract Peano structure of
517`LogicNat` is the orbit structure of any non-trivial element under
518multiplication.
519
520The full chain (existence of γ from `non_trivial`, injectivity of the
521embedding from the J-cost positivity off-identity, generator-free
522characterization of the embedding's image) is left for Level 2. The
523content of this section is the embedding map and its multiplicative
524homomorphism property. -/
525
526/-- A non-trivial generator: any positive real other than the
527identity. The Law of Logic guarantees existence via the
528`non_trivial` field of `SatisfiesLawsOfLogic`. -/
used by (40)
-
aestronglyMeasurable_galerkinForcing_mode_of_continuous -
hasDerivAt_extendByZero_apply -
decodeCoeff -
isCalibrated_of_isCalibratedLimit -
washburn_uniqueness -
xFlatConnection -
T5_uniqueness_complete -
Jcost_log_second_deriv_normalized -
love_eliminates_all_waste -
embed_injective -
eq_iff_toNat_eq -
FiniteDescriptionRegularity -
embedState -
embedState_injective -
F_forced_to_Jcost -
bilinear_family_forced -
J_computes_P -
log_aczel_data_of_laws -
log_bilinear_affine_lift_classification -
log_bilinear_positive_cost_bilinear -
ledger_symmetry_negative_rungs -
RecognitionStep -
response_limit_high_freq -
response_function_is_real_part -
dirichlet_eq_neg_quadratic -
orientedToRatio -
toricCode -
fromZ_one -
Z -
current_chain_distinct