59structure GeometricScaleSequence where 60 ratio : ℝ 61 ratio_pos : 0 < ratio 62 ratio_ne_one : ratio ≠ 1 -- Non-trivial scaling 63 64/-- The n-th scale in the sequence -/ 65noncomputable def GeometricScaleSequence.scale (S : GeometricScaleSequence) (n : ℕ) : ℝ :=
proof body
Definition body.
66 S.ratio ^ n 67 68/-- All scales are positive -/ 69lemma GeometricScaleSequence.scale_pos (S : GeometricScaleSequence) (n : ℕ) : 70 0 < S.scale n := by 71 unfold GeometricScaleSequence.scale 72 exact pow_pos S.ratio_pos n 73 74/-! ## Axiom 2: Additive Ledger Composition 75 76When two recognition events combine, their scales add. 77 78This is motivated by: 791. J-cost is additive: J_total = J(a) + J(b) 802. The ledger tracks "total work," which sums contributions 813. This matches the Fibonacci-like "next = current + previous" pattern 82-/ 83 84/-- The composition of two scales is their sum -/
used by (11)
From the project-wide theorem graph. These declarations reference this one in their body.