IndisputableMonolith.Foundation.LedgerToFactorization
IndisputableMonolith/Foundation/LedgerToFactorization.lean · 887 lines · 46 declarations
show as:
view math explainer →
1import IndisputableMonolith.Foundation.RecognitionLedgerFloor
2import IndisputableMonolith.Foundation.DAlembert.FactorizationForcing
3
4/-!
5# Ledger to Factorization Bridge
6
7Phase 3 asks for the T4-to-T5 bridge to be derived from the recognition ledger
8rather than assumed as an analytic input. This file isolates the precise
9remaining algebraic condition.
10
11The free ledger already proves unconditional additivity. If a two-variable
12combiner has the corresponding ledger-linear response in its second argument,
13then the `rightAffine` field used by the d'Alembert factorization gate follows.
14Together with symmetry, the boundary law, and the unit diagonal, the existing
15gate theorem forces the RCL polynomial.
16-/
17
18namespace IndisputableMonolith
19namespace Foundation
20namespace LedgerToFactorization
21
22open DAlembert.FactorizationForcing
23
24/-- Monotone additive real responses are linear. This is the order-regularity
25replacement for the continuity gate in the additive Cauchy step. -/
26theorem monotone_additive_isLinear {f : ℝ → ℝ}
27 (hadd : ∀ x y, f (x + y) = f x + f y) (hmono : Monotone f) :
28 ∀ x, f x = f 1 * x := by
29 have hf0 : f 0 = 0 := by
30 have h := hadd 0 0
31 rw [add_zero] at h
32 linarith
33 let F : ℝ →+ ℝ := AddMonoidHom.mk' f (fun a b => hadd a b)
34 have hFcoe : ∀ y, F y = f y := fun _ => rfl
35 have hFq : ∀ q : ℚ, f (q : ℝ) = f 1 * (q : ℝ) := by
36 intro q
37 have h := map_ratCast_smul F ℝ ℝ q (1 : ℝ)
38 simp only [smul_eq_mul, mul_one, hFcoe] at h
39 rw [h]
40 ring
41 intro x
42 set c := f 1 with hc_def
43 have hc : 0 ≤ c := by
44 have hmle : f 0 ≤ f 1 := hmono (by norm_num)
45 rw [hf0] at hmle
46 exact hmle
47 rcases eq_or_lt_of_le hc with hc0 | hcpos
48 · have hub : f x ≤ 0 := by
49 obtain ⟨r, hxr, -⟩ := exists_rat_btwn (lt_add_one x)
50 have hmr := hmono hxr.le
51 rw [hFq r, ← hc0, zero_mul] at hmr
52 exact hmr
53 have hlb : 0 ≤ f x := by
54 obtain ⟨q, -, hqx⟩ := exists_rat_btwn (sub_one_lt x)
55 have hmq := hmono hqx.le
56 rw [hFq q, ← hc0, zero_mul] at hmq
57 exact hmq
58 rw [← hc0, zero_mul]
59 linarith
60 · refine le_antisymm ?_ ?_
61 · by_contra hcon
62 push_neg at hcon
63 have hxlt : x < f x / c := by
64 rw [lt_div_iff₀ hcpos]
65 linarith [mul_comm c x]
66 obtain ⟨r, hxr, hrlt⟩ := exists_rat_btwn hxlt
67 have h1 : f x ≤ c * (r : ℝ) := by
68 have hm := hmono hxr.le
69 rwa [hFq r] at hm
70 have h2 : c * (r : ℝ) < f x := by
71 have := (lt_div_iff₀ hcpos).mp hrlt
72 linarith [mul_comm (r : ℝ) c]
73 linarith
74 · by_contra hcon
75 push_neg at hcon
76 have hxlt : f x / c < x := by
77 rw [div_lt_iff₀ hcpos]
78 linarith [mul_comm c x]
79 obtain ⟨q, hqlt, hqx⟩ := exists_rat_btwn hxlt
80 have h1 : c * (q : ℝ) ≤ f x := by
81 have hm := hmono hqx.le
82 rwa [hFq q] at hm
83 have h2 : f x < c * (q : ℝ) := by
84 have := (div_lt_iff₀ hcpos).mp hqlt
85 linarith [mul_comm (q : ℝ) c]
86 linarith
87
88/-- Antitone additive real responses are linear. Apply the monotone lemma to
89`-f`. This is the second branch of the directional (order) regularity route:
90the RCL response slope `2(u+1)` is negative for `u < -1`, so the response is
91antitone there, not monotone. -/
92theorem antitone_additive_isLinear {f : ℝ → ℝ}
93 (hadd : ∀ x y, f (x + y) = f x + f y) (hanti : Antitone f) :
94 ∀ x, f x = f 1 * x := by
95 have hadd' : ∀ x y, (fun t => -f t) (x + y) =
96 (fun t => -f t) x + (fun t => -f t) y := by
97 intro x y
98 simp only [hadd x y]
99 ring
100 have hmono' : Monotone (fun t => -f t) := by
101 intro a b hab
102 simp only [neg_le_neg_iff]
103 exact hanti hab
104 have h := monotone_additive_isLinear hadd' hmono'
105 intro x
106 have hx : -f x = -f 1 * x := h x
107 have hx2 : -f x = -(f 1 * x) := by rw [hx]; ring
108 linarith
109
110/-- An additive real response that never decreases cost on non-negatively posted
111mass is monotone everywhere. This is the order shadow of `ledgerCost_nonneg`:
112adding defect mass `b - a ≥ 0` adds non-negative cost, so the response is
113non-decreasing. No continuity or completeness is used. -/
114theorem additive_nonnegOnNonneg_isMonotone {f : ℝ → ℝ}
115 (hadd : ∀ x y, f (x + y) = f x + f y)
116 (hnn : ∀ x, 0 ≤ x → 0 ≤ f x) : Monotone f := by
117 have hf0 : f 0 = 0 := by
118 have h := hadd 0 0
119 rw [add_zero] at h
120 linarith
121 intro a b hab
122 have hsub : f b = f (b - a) + f a := by
123 have h := hadd (b - a) a
124 rw [sub_add_cancel] at h
125 exact h
126 have hnn' : 0 ≤ f (b - a) := hnn (b - a) (by linarith)
127 linarith
128
129/-- Ledger-linear response for a combiner: the second argument is governed by
130its response to one unit of posted ledger mass. The `free_ledger_additivity`
131field pins this bridge to the existing free-ledger theorem rather than leaving
132it as prose. -/
133structure LedgerLinearResponse (P : ℝ → ℝ → ℝ) : Prop where
134 symmetric : ∀ u v, P u v = P v u
135 zeroBoundary : ∀ u, P u 0 = 2 * u
136 unitDiagonal : P 1 1 = 6
137 rightResponse :
138 ∀ u v, P u v = (P u 1 - P u 0) * v + P u 0
139 free_ledger_additivity :
140 ∀ (I : Type) (w : I → ℝ)
141 (Γ Δ : RecognitionLedgerFloor.DefectLedger I),
142 RecognitionLedgerFloor.ledgerCost w (Γ + Δ) =
143 RecognitionLedgerFloor.ledgerCost w Γ +
144 RecognitionLedgerFloor.ledgerCost w Δ
145
146/-- Free-ledger semantics for a candidate factorization combiner. The response
147law is intentionally weaker than `LedgerLinearResponse`: it records additive
148posting in the second coordinate plus a regularity gate, leaving Cauchy
149linearization as a theorem rather than a field. -/
150structure FreeLedgerCombinerSemantics (P : ℝ → ℝ → ℝ) : Prop where
151 symmetric : ∀ u v, P u v = P v u
152 zeroBoundary : ∀ u, P u 0 = 2 * u
153 unitDiagonal : P 1 1 = 6
154 rightPostedAdditive :
155 ∀ u v w,
156 P u (v + w) - P u 0 =
157 (P u v - P u 0) + (P u w - P u 0)
158 rightContinuous : ∀ u, Continuous fun v => P u v
159 free_ledger_additivity :
160 ∀ (I : Type) (w : I → ℝ)
161 (Γ Δ : RecognitionLedgerFloor.DefectLedger I),
162 RecognitionLedgerFloor.ledgerCost w (Γ + Δ) =
163 RecognitionLedgerFloor.ledgerCost w Γ +
164 RecognitionLedgerFloor.ledgerCost w Δ
165
166/-- Primitive ledger-posting semantics: the second coordinate is fed directly by
167the cost of actual free defect ledgers, and posting ledgers additively is the
168operation seen by the combiner. This is closer to the Phase-2 ledger than the
169`DiscreteLedgerPostingSemantics` surface, which only talks about natural-number
170costs after choosing the rank-one unit ledger. -/
171structure PrimitiveLedgerPostingSemantics (P : ℝ → ℝ → ℝ) : Prop where
172 symmetric : ∀ u v, P u v = P v u
173 zeroBoundary : ∀ u, P u 0 = 2 * u
174 unitDiagonal : P 1 1 = 6
175 rightLedgerPostedAdditive :
176 ∀ (u : ℝ) (I : Type) (w : I → ℝ)
177 (Γ Δ : RecognitionLedgerFloor.DefectLedger I),
178 P u (RecognitionLedgerFloor.ledgerCost w (Γ + Δ)) - P u 0 =
179 (P u (RecognitionLedgerFloor.ledgerCost w Γ) - P u 0) +
180 (P u (RecognitionLedgerFloor.ledgerCost w Δ) - P u 0)
181 free_ledger_additivity :
182 ∀ (I : Type) (w : I → ℝ)
183 (Γ Δ : RecognitionLedgerFloor.DefectLedger I),
184 RecognitionLedgerFloor.ledgerCost w (Γ + Δ) =
185 RecognitionLedgerFloor.ledgerCost w Γ +
186 RecognitionLedgerFloor.ledgerCost w Δ
187
188/-- Primitive ledger posting over arbitrary weighted defect ledgers gives the
189additive response law for arbitrary real postings. -/
190theorem primitiveLedgerPosting_forces_rightPostedAdditive
191 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P) :
192 ∀ u v w,
193 P u (v + w) - P u 0 =
194 (P u v - P u 0) + (P u w - P u 0) := by
195 intro u v w
196 let weight : Bool → ℝ := fun b => if b then w else v
197 let Γ : RecognitionLedgerFloor.DefectLedger Bool := Finsupp.single false 1
198 let Δ : RecognitionLedgerFloor.DefectLedger Bool := Finsupp.single true 1
199 have hpost := h.rightLedgerPostedAdditive u Bool weight Γ Δ
200 have hΓ : RecognitionLedgerFloor.ledgerCost weight Γ = v := by
201 simp [Γ, weight, RecognitionLedgerFloor.ledgerCost_single]
202 have hΔ : RecognitionLedgerFloor.ledgerCost weight Δ = w := by
203 simp [Δ, weight, RecognitionLedgerFloor.ledgerCost_single]
204 have hsum : RecognitionLedgerFloor.ledgerCost weight (Γ + Δ) = v + w := by
205 rw [RecognitionLedgerFloor.ledgerCost_add, hΓ, hΔ]
206 simpa [hΓ, hΔ, hsum] using hpost
207
208/-- Primitive ledger posting plus continuity gives the completed free-ledger
209posting semantics. The additive response law is no longer a separate
210assumption: realize arbitrary real postings `v` and `w` as the costs of two
211primitive defects in a two-generator ledger. -/
212theorem freeLedgerCombinerSemantics_from_primitiveLedgerPosting
213 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
214 (hcont : ∀ u, Continuous fun v => P u v) :
215 FreeLedgerCombinerSemantics P := by
216 refine {
217 symmetric := h.symmetric
218 zeroBoundary := h.zeroBoundary
219 unitDiagonal := h.unitDiagonal
220 rightPostedAdditive := ?_
221 rightContinuous := hcont
222 free_ledger_additivity := h.free_ledger_additivity
223 }
224 exact primitiveLedgerPosting_forces_rightPostedAdditive P h
225
226/-- Discrete posting semantics on the actual rank-one ledger-cost surface.
227The second coordinate is restricted to natural-number ledger costs, i.e. the
228values produced by finite multiplicities before analytic completion. -/
229structure DiscreteLedgerPostingSemantics (P : ℝ → ℝ → ℝ) : Prop where
230 symmetric : ∀ u v, P u v = P v u
231 zeroBoundary : ∀ u, P u 0 = 2 * u
232 unitDiagonal : P 1 1 = 6
233 rightNatPostedAdditive :
234 ∀ (u : ℝ) (m n : ℕ),
235 P u ((m + n : ℕ) : ℝ) - P u 0 =
236 (P u (m : ℝ) - P u 0) + (P u (n : ℝ) - P u 0)
237 free_ledger_additivity :
238 ∀ (I : Type) (w : I → ℝ)
239 (Γ Δ : RecognitionLedgerFloor.DefectLedger I),
240 RecognitionLedgerFloor.ledgerCost w (Γ + Δ) =
241 RecognitionLedgerFloor.ledgerCost w Γ +
242 RecognitionLedgerFloor.ledgerCost w Δ
243
244/-- Primitive ledger posting specializes to the natural-number rank-one ledger
245surface. -/
246theorem discreteLedgerPosting_from_primitiveLedgerPosting
247 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P) :
248 DiscreteLedgerPostingSemantics P := by
249 refine {
250 symmetric := h.symmetric
251 zeroBoundary := h.zeroBoundary
252 unitDiagonal := h.unitDiagonal
253 rightNatPostedAdditive := ?_
254 free_ledger_additivity := h.free_ledger_additivity
255 }
256 intro u m n
257 let Γ : RecognitionLedgerFloor.DefectLedger Unit := Finsupp.single () m
258 let Δ : RecognitionLedgerFloor.DefectLedger Unit := Finsupp.single () n
259 have hpost := h.rightLedgerPostedAdditive u Unit (fun _ : Unit => (1 : ℝ)) Γ Δ
260 have hΓ :
261 RecognitionLedgerFloor.ledgerCost (fun _ : Unit => (1 : ℝ)) Γ = (m : ℝ) := by
262 simpa [Γ] using RecognitionLedgerFloor.unit_cost_is_generator_count (I := Unit) () m
263 have hΔ :
264 RecognitionLedgerFloor.ledgerCost (fun _ : Unit => (1 : ℝ)) Δ = (n : ℝ) := by
265 simpa [Δ] using RecognitionLedgerFloor.unit_cost_is_generator_count (I := Unit) () n
266 have hsum :
267 RecognitionLedgerFloor.ledgerCost (fun _ : Unit => (1 : ℝ)) (Γ + Δ) =
268 ((m + n : ℕ) : ℝ) := by
269 rw [RecognitionLedgerFloor.ledgerCost_add, hΓ, hΔ]
270 norm_num
271 simpa [hΓ, hΔ, hsum] using hpost
272
273/-- Rational posting semantics on the countable positive-ratio completion of
274the free ledger. This is the analytic-completion input: rational ledger costs
275already follow the affine response law, and the response is continuous in the
276completed real coordinate. -/
277structure RationalLedgerPostingSemantics (P : ℝ → ℝ → ℝ) : Prop where
278 symmetric : ∀ u v, P u v = P v u
279 zeroBoundary : ∀ u, P u 0 = 2 * u
280 unitDiagonal : P 1 1 = 6
281 rightContinuous : ∀ u, Continuous fun v => P u v
282 rightRatAffine :
283 ∀ (u : ℝ) (q : ℚ),
284 P u (q : ℝ) - P u 0 = (q : ℝ) * (P u 1 - P u 0)
285 free_ledger_additivity :
286 ∀ (I : Type) (w : I → ℝ)
287 (Γ Δ : RecognitionLedgerFloor.DefectLedger I),
288 RecognitionLedgerFloor.ledgerCost w (Γ + Δ) =
289 RecognitionLedgerFloor.ledgerCost w Γ +
290 RecognitionLedgerFloor.ledgerCost w Δ
291
292/-- Discrete ledger posting forces affine response on the actual
293natural-number ledger-cost surface. This is the finite-ledger version of
294right-affineness: no real-continuum completion is used here. -/
295theorem discreteLedgerPosting_forces_natAffineResponse
296 (P : ℝ → ℝ → ℝ) (h : DiscreteLedgerPostingSemantics P) :
297 ∀ u (n : ℕ),
298 P u (n : ℝ) = (P u 1 - P u 0) * (n : ℝ) + P u 0 := by
299 intro u n
300 let R : ℕ → ℝ := fun k => P u (k : ℝ) - P u 0
301 have hRadd : ∀ m n : ℕ, R (m + n) = R m + R n := by
302 intro m n
303 exact h.rightNatPostedAdditive u m n
304 have hR : ∀ n : ℕ, R n = (n : ℝ) * R 1 := by
305 intro n
306 induction n with
307 | zero =>
308 simp [R]
309 | succ n ih =>
310 have hstep : R (n + 1) = R n + R 1 := hRadd n 1
311 have hsucc : R (Nat.succ n) = R n + R 1 := by
312 simpa [Nat.succ_eq_add_one] using hstep
313 rw [hsucc, ih]
314 norm_num
315 ring
316 have hRn : P u (n : ℝ) - P u 0 = (n : ℝ) * (P u 1 - P u 0) := by
317 simpa [R] using hR n
318 have hcomm :
319 (n : ℝ) * (P u 1 - P u 0) =
320 (P u 1 - P u 0) * (n : ℝ) := by
321 ring
322 linarith
323
324/-- Primitive ledger posting already forces affine response on the actual
325natural-number rank-one ledger-cost surface. -/
326theorem primitiveLedgerPosting_forces_natAffineResponse
327 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P) :
328 ∀ u (n : ℕ),
329 P u (n : ℝ) = (P u 1 - P u 0) * (n : ℝ) + P u 0 :=
330 discreteLedgerPosting_forces_natAffineResponse P
331 (discreteLedgerPosting_from_primitiveLedgerPosting P h)
332
333/-- The canonical RCL combiner carries the discrete free-ledger posting
334semantics before analytic completion. -/
335theorem rclCombiner_discreteLedgerPostingSemantics :
336 DiscreteLedgerPostingSemantics rclCombiner where
337 symmetric := rclCombiner_satisfies_gate.symmetric
338 zeroBoundary := rclCombiner_satisfies_gate.zeroBoundary
339 unitDiagonal := rclCombiner_satisfies_gate.unitDiagonal
340 rightNatPostedAdditive := by
341 intro u m n
342 unfold rclCombiner
343 norm_num
344 ring
345 free_ledger_additivity := by
346 intro I w Γ Δ
347 exact RecognitionLedgerFloor.ledgerCost_add w Γ Δ
348
349/-- The canonical RCL combiner satisfies the primitive free-ledger posting law
350before passing to the rank-one natural-number surface. -/
351theorem rclCombiner_primitiveLedgerPostingSemantics :
352 PrimitiveLedgerPostingSemantics rclCombiner where
353 symmetric := rclCombiner_satisfies_gate.symmetric
354 zeroBoundary := rclCombiner_satisfies_gate.zeroBoundary
355 unitDiagonal := rclCombiner_satisfies_gate.unitDiagonal
356 rightLedgerPostedAdditive := by
357 intro u I w Γ Δ
358 rw [RecognitionLedgerFloor.ledgerCost_add]
359 unfold rclCombiner
360 ring
361 free_ledger_additivity := by
362 intro I w Γ Δ
363 exact RecognitionLedgerFloor.ledgerCost_add w Γ Δ
364
365/-- Rational ledger posting plus continuity completes the response from the
366dense rational ledger-ratio surface to all real completed costs. -/
367theorem ledgerLinearResponse_from_rationalLedgerPosting
368 (P : ℝ → ℝ → ℝ) (h : RationalLedgerPostingSemantics P) :
369 LedgerLinearResponse P := by
370 refine {
371 symmetric := h.symmetric
372 zeroBoundary := h.zeroBoundary
373 unitDiagonal := h.unitDiagonal
374 rightResponse := ?_
375 free_ledger_additivity := h.free_ledger_additivity
376 }
377 intro u v
378 let f : ℝ → ℝ := fun x => P u x - P u 0
379 let g : ℝ → ℝ := fun x => x * (P u 1 - P u 0)
380 have hf : Continuous f := by
381 exact (h.rightContinuous u).sub continuous_const
382 have hg : Continuous g := by
383 exact continuous_id.mul continuous_const
384 have hdense : DenseRange (fun q : ℚ => (q : ℝ)) :=
385 Rat.denseRange_cast
386 have hfg : f = g := by
387 refine DenseRange.equalizer hdense hf hg ?_
388 funext q
389 exact h.rightRatAffine u q
390 have hv := congrFun hfg v
391 change P u v - P u 0 = v * (P u 1 - P u 0) at hv
392 have hcomm : v * (P u 1 - P u 0) = (P u 1 - P u 0) * v := by
393 ring
394 linarith
395
396/-- The canonical RCL combiner satisfies the rational completed posting
397semantics. -/
398theorem rclCombiner_rationalLedgerPostingSemantics :
399 RationalLedgerPostingSemantics rclCombiner where
400 symmetric := rclCombiner_satisfies_gate.symmetric
401 zeroBoundary := rclCombiner_satisfies_gate.zeroBoundary
402 unitDiagonal := rclCombiner_satisfies_gate.unitDiagonal
403 rightContinuous := by
404 intro u
405 unfold rclCombiner
406 continuity
407 rightRatAffine := by
408 intro u q
409 unfold rclCombiner
410 norm_num
411 ring
412 free_ledger_additivity := by
413 intro I w Γ Δ
414 exact RecognitionLedgerFloor.ledgerCost_add w Γ Δ
415
416/-- Completed ledger-linear response is exactly rational ledger posting plus
417continuity. The forward direction is algebraic; the reverse direction is the
418dense-rational completion theorem above. -/
419theorem rationalLedgerPosting_iff_ledgerLinearResponse (P : ℝ → ℝ → ℝ) :
420 RationalLedgerPostingSemantics P ↔ LedgerLinearResponse P := by
421 constructor
422 · exact ledgerLinearResponse_from_rationalLedgerPosting P
423 · intro h
424 refine {
425 symmetric := h.symmetric
426 zeroBoundary := h.zeroBoundary
427 unitDiagonal := h.unitDiagonal
428 rightContinuous := ?_
429 rightRatAffine := ?_
430 free_ledger_additivity := h.free_ledger_additivity
431 }
432 · intro u
433 have hfun :
434 (fun v => P u v) =
435 fun v => (P u 1 - P u 0) * v + P u 0 := by
436 funext v
437 exact h.rightResponse u v
438 rw [hfun]
439 exact (continuous_const.mul continuous_id).add continuous_const
440 · intro u q
441 rw [h.rightResponse u (q : ℝ)]
442 ring
443
444/-- Continuous additive posting response is linear over `ℝ`, so free-ledger
445semantics supplies the exact `LedgerLinearResponse` bridge. -/
446theorem ledgerLinearResponse_from_free_ledger
447 (P : ℝ → ℝ → ℝ) (h : FreeLedgerCombinerSemantics P) :
448 LedgerLinearResponse P := by
449 refine {
450 symmetric := h.symmetric
451 zeroBoundary := h.zeroBoundary
452 unitDiagonal := h.unitDiagonal
453 rightResponse := ?_
454 free_ledger_additivity := h.free_ledger_additivity
455 }
456 intro u v
457 let response : ℝ →+ ℝ := {
458 toFun := fun t => P u t - P u 0
459 map_zero' := by ring
460 map_add' := by
461 intro a b
462 exact h.rightPostedAdditive u a b
463 }
464 have hresponse_cont : Continuous response := by
465 change Continuous fun t => P u t - P u 0
466 exact (h.rightContinuous u).sub continuous_const
467 let linearResponse : ℝ →L[ℝ] ℝ :=
468 AddMonoidHom.toRealLinearMap response hresponse_cont
469 have hlinear :
470 response v = v * response 1 := by
471 have hsmul := linearResponse.map_smul v 1
472 change response (v * 1) = v * response 1 at hsmul
473 simpa using hsmul
474 change P u v = (P u 1 - P u 0) * v + P u 0
475 have hcomm : v * (P u 1 - P u 0) = (P u 1 - P u 0) * v := by ring
476 have hsub : P u v - P u 0 = (P u 1 - P u 0) * v := by
477 simpa [response, hcomm] using hlinear
478 linarith
479
480/-- Primitive ledger posting plus continuity forces completed real
481ledger-linear response. -/
482theorem ledgerLinearResponse_from_primitiveLedgerPosting
483 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
484 (hcont : ∀ u, Continuous fun v => P u v) :
485 LedgerLinearResponse P :=
486 ledgerLinearResponse_from_free_ledger P
487 (freeLedgerCombinerSemantics_from_primitiveLedgerPosting P h hcont)
488
489/-- Primitive ledger posting plus a *globally* monotone response gives completed
490real ledger-linear response. WARNING (honesty): the global-monotone hypothesis
491is vacuous for the target combiner: the forced conclusion is RCL, whose response
492slope `2(u+1)` is negative for `u < -1`, so no `P` satisfies both this hypothesis
493and the conclusion. The genuine, non-vacuous order route is
494`ledgerLinearResponse_from_primitiveLedgerPosting_directional` below (monotone OR
495antitone per slice); this monotone-only form is kept as a special case and as a
496proof component, and is non-vacuous only on the physical cost cone `u ≥ -1`. -/
497theorem ledgerLinearResponse_from_primitiveLedgerPosting_monotone
498 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
499 (hmono : ∀ u, Monotone fun v => P u v) :
500 LedgerLinearResponse P := by
501 refine {
502 symmetric := h.symmetric
503 zeroBoundary := h.zeroBoundary
504 unitDiagonal := h.unitDiagonal
505 rightResponse := ?_
506 free_ledger_additivity := h.free_ledger_additivity
507 }
508 intro u v
509 let response : ℝ → ℝ := fun t => P u t - P u 0
510 have hadd : ∀ x y, response (x + y) = response x + response y := by
511 intro x y
512 exact primitiveLedgerPosting_forces_rightPostedAdditive P h u x y
513 have hresponse_mono : Monotone response := by
514 intro a b hab
515 exact sub_le_sub_right ((hmono u) hab) (P u 0)
516 have hlin := monotone_additive_isLinear hadd hresponse_mono v
517 have hsub : P u v - P u 0 = (P u 1 - P u 0) * v := by
518 simpa [response] using hlin
519 linarith
520
521/-- Primitive ledger posting plus **global** cost non-negativity gives completed
522real ledger-linear response. WARNING (honesty): like the monotone form above,
523the *global* non-negativity hypothesis (`P u 0 ≤ P u v` for all `u`, all `v ≥ 0`)
524is vacuous for the target combiner; RCL fails it for `u < -1`. It holds on the
525physical cost cone `u ≥ 0` (`rclCombiner_postingNonneg`), where it is the genuine
526order shadow of `ledgerCost_nonneg`. For the non-vacuous global closure use
527`ledgerLinearResponse_from_primitiveLedgerPosting_directional`. -/
528theorem ledgerLinearResponse_from_primitiveLedgerPosting_nonneg
529 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
530 (hnn : ∀ u v, 0 ≤ v → P u 0 ≤ P u v) :
531 LedgerLinearResponse P := by
532 refine ledgerLinearResponse_from_primitiveLedgerPosting_monotone P h ?_
533 intro u
534 have hadd : ∀ x y,
535 (fun v => P u v - P u 0) (x + y) =
536 (fun v => P u v - P u 0) x + (fun v => P u v - P u 0) y := by
537 intro x y
538 exact primitiveLedgerPosting_forces_rightPostedAdditive P h u x y
539 have hfnn : ∀ x, 0 ≤ x → 0 ≤ (fun v => P u v - P u 0) x := by
540 intro x hx
541 have := hnn u x hx
542 simp only
543 linarith
544 have hmono := additive_nonnegOnNonneg_isMonotone hadd hfnn
545 intro a b hab
546 have hle := hmono hab
547 simp only at hle
548 linarith
549
550/-- Primitive ledger posting plus **per-slice directional regularity** forces the
551completed real ledger-linear response. For each fixed first cost `u`, the
552combined cost responds to posted mass `v` in one consistent order direction
553(monotone or antitone). This is the genuine, non-vacuous order replacement for
554the analytic continuity gate: unlike global monotonicity, the canonical RCL
555combiner provably satisfies this (its response slope `2(u+1)` has a fixed sign
556for each `u`), so the forcing hypothesis is consistent with its conclusion. -/
557theorem ledgerLinearResponse_from_primitiveLedgerPosting_directional
558 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
559 (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v)) :
560 LedgerLinearResponse P := by
561 refine {
562 symmetric := h.symmetric
563 zeroBoundary := h.zeroBoundary
564 unitDiagonal := h.unitDiagonal
565 rightResponse := ?_
566 free_ledger_additivity := h.free_ledger_additivity
567 }
568 intro u v
569 let response : ℝ → ℝ := fun t => P u t - P u 0
570 have hadd : ∀ x y, response (x + y) = response x + response y := by
571 intro x y
572 exact primitiveLedgerPosting_forces_rightPostedAdditive P h u x y
573 have hlin : ∀ x, response x = response 1 * x := by
574 rcases hdir u with hmono | hanti
575 · have hrmono : Monotone response := by
576 intro a b hab
577 exact sub_le_sub_right (hmono hab) (P u 0)
578 exact monotone_additive_isLinear hadd hrmono
579 · have hranti : Antitone response := by
580 intro a b hab
581 exact sub_le_sub_right (hanti hab) (P u 0)
582 exact antitone_additive_isLinear hadd hranti
583 have hsub : P u v - P u 0 = (P u 1 - P u 0) * v := by
584 simpa [response] using hlin v
585 linarith
586
587/-- Completed ledger-linear response is exactly free-ledger posting semantics
588plus continuity. -/
589theorem freeLedgerCombinerSemantics_iff_ledgerLinearResponse (P : ℝ → ℝ → ℝ) :
590 FreeLedgerCombinerSemantics P ↔ LedgerLinearResponse P := by
591 constructor
592 · exact ledgerLinearResponse_from_free_ledger P
593 · intro h
594 refine {
595 symmetric := h.symmetric
596 zeroBoundary := h.zeroBoundary
597 unitDiagonal := h.unitDiagonal
598 rightPostedAdditive := ?_
599 rightContinuous := ?_
600 free_ledger_additivity := h.free_ledger_additivity
601 }
602 · intro u v w
603 rw [h.rightResponse u (v + w), h.rightResponse u v, h.rightResponse u w]
604 ring
605 · intro u
606 have hfun :
607 (fun v => P u v) =
608 fun v => (P u 1 - P u 0) * v + P u 0 := by
609 funext v
610 exact h.rightResponse u v
611 rw [hfun]
612 exact (continuous_const.mul continuous_id).add continuous_const
613
614/-- Ledger-linear response supplies the `rightAffine` field of the
615factorization gate. -/
616theorem rightAffine_of_ledgerLinearResponse
617 (P : ℝ → ℝ → ℝ) (h : LedgerLinearResponse P) :
618 ∀ u, ∃ α β, ∀ v, P u v = α * v + β := by
619 intro u
620 exact ⟨P u 1 - P u 0, P u 0, h.rightResponse u⟩
621
622/-- Ledger-linear response plus the remaining gate fields gives the full
623factorization gate. -/
624theorem factorizationGate_of_ledgerLinearResponse
625 (P : ℝ → ℝ → ℝ) (h : LedgerLinearResponse P) :
626 FactorizationAssociativityGate P where
627 symmetric := h.symmetric
628 rightAffine := rightAffine_of_ledgerLinearResponse P h
629 zeroBoundary := h.zeroBoundary
630 unitDiagonal := h.unitDiagonal
631
632/-- Ledger-linear response forces the RCL polynomial through the existing gate
633theorem. -/
634theorem ledgerLinearResponse_forces_rcl
635 (P : ℝ → ℝ → ℝ) (h : LedgerLinearResponse P) :
636 ∀ u v, P u v = rclCombiner u v := by
637 intro u v
638 rw [gate_forces_rcl P (factorizationGate_of_ledgerLinearResponse P h) u v]
639 rfl
640
641/-- Primitive ledger posting plus continuity supplies the full factorization
642gate. -/
643theorem factorizationGate_of_primitiveLedgerPosting
644 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
645 (hcont : ∀ u, Continuous fun v => P u v) :
646 FactorizationAssociativityGate P :=
647 factorizationGate_of_ledgerLinearResponse P
648 (ledgerLinearResponse_from_primitiveLedgerPosting P h hcont)
649
650/-- Primitive ledger posting plus continuity forces the canonical RCL
651combiner. -/
652theorem primitiveLedgerPosting_forces_rcl
653 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
654 (hcont : ∀ u, Continuous fun v => P u v) :
655 ∀ u v, P u v = rclCombiner u v :=
656 ledgerLinearResponse_forces_rcl P
657 (ledgerLinearResponse_from_primitiveLedgerPosting P h hcont)
658
659/-- Primitive ledger posting plus monotone response supplies the full
660factorization gate. This is the order-regularity route: monotonicity replaces
661the continuity gate. -/
662theorem factorizationGate_of_primitiveLedgerPosting_monotone
663 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
664 (hmono : ∀ u, Monotone fun v => P u v) :
665 FactorizationAssociativityGate P :=
666 factorizationGate_of_ledgerLinearResponse P
667 (ledgerLinearResponse_from_primitiveLedgerPosting_monotone P h hmono)
668
669/-- Primitive ledger posting plus monotone response forces the canonical RCL
670combiner. No continuity or completeness is used: only additivity from the free
671ledger and order regularity. -/
672theorem primitiveLedgerPosting_monotone_forces_rcl
673 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
674 (hmono : ∀ u, Monotone fun v => P u v) :
675 ∀ u v, P u v = rclCombiner u v :=
676 ledgerLinearResponse_forces_rcl P
677 (ledgerLinearResponse_from_primitiveLedgerPosting_monotone P h hmono)
678
679/-- Primitive ledger posting plus **ledger-native cost non-negativity** supplies
680the full factorization gate. The regularity input is the order shadow of
681`ledgerCost_nonneg`, not an analytic continuity assumption. -/
682theorem factorizationGate_of_primitiveLedgerPosting_nonneg
683 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
684 (hnn : ∀ u v, 0 ≤ v → P u 0 ≤ P u v) :
685 FactorizationAssociativityGate P :=
686 factorizationGate_of_ledgerLinearResponse P
687 (ledgerLinearResponse_from_primitiveLedgerPosting_nonneg P h hnn)
688
689/-- Primitive ledger posting plus **ledger-native cost non-negativity** forces the
690canonical RCL combiner. This is the fully ledger-internal route to
691right-affineness: additivity comes from `ledgerCost_add`, and the only order
692input is that posting non-negative defect mass never lowers cost, which is the
693order shadow of `ledgerCost_nonneg`. -/
694theorem primitiveLedgerPosting_nonneg_forces_rcl
695 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
696 (hnn : ∀ u v, 0 ≤ v → P u 0 ≤ P u v) :
697 ∀ u v, P u v = rclCombiner u v :=
698 ledgerLinearResponse_forces_rcl P
699 (ledgerLinearResponse_from_primitiveLedgerPosting_nonneg P h hnn)
700
701/-- Primitive ledger posting plus **per-slice directional regularity** supplies
702the full factorization gate. This is the non-vacuous order route: the canonical
703combiner satisfies the hypothesis (`rclCombiner_directional`). -/
704theorem factorizationGate_of_primitiveLedgerPosting_directional
705 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
706 (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v)) :
707 FactorizationAssociativityGate P :=
708 factorizationGate_of_ledgerLinearResponse P
709 (ledgerLinearResponse_from_primitiveLedgerPosting_directional P h hdir)
710
711/-- Primitive ledger posting plus **per-slice directional regularity** forces the
712canonical RCL combiner. Additivity is supplied by `ledgerCost_add`; the only
713regularity input is that each fixed-cost response is monotone in one direction,
714which the canonical combiner provably satisfies, so this forcing is
715non-vacuous. -/
716theorem primitiveLedgerPosting_directional_forces_rcl
717 (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
718 (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v)) :
719 ∀ u v, P u v = rclCombiner u v :=
720 ledgerLinearResponse_forces_rcl P
721 (ledgerLinearResponse_from_primitiveLedgerPosting_directional P h hdir)
722
723/-- **Ledger order-faithfulness anchor.** For non-negative weights the free
724ledger cost never decreases when defect mass is added. This is a direct
725consequence of unconditional additivity (`ledgerCost_add`) and cost
726non-negativity (`ledgerCost_nonneg`); it is the proved ledger fact whose order
727shadow is the `hnn` hypothesis of the non-negativity route above. -/
728theorem ledgerCost_le_add_right {I : Type} (w : I → ℝ) (hw : ∀ i, 0 ≤ w i)
729 (Γ Δ : RecognitionLedgerFloor.DefectLedger I) :
730 RecognitionLedgerFloor.ledgerCost w Γ ≤
731 RecognitionLedgerFloor.ledgerCost w (Γ + Δ) := by
732 rw [RecognitionLedgerFloor.ledgerCost_add]
733 linarith [RecognitionLedgerFloor.ledgerCost_nonneg w hw Δ]
734
735/-- The canonical RCL combiner satisfies the ledger-native posting
736non-negativity hypothesis on the physical recognition domain `u ≥ 0`: posting
737non-negative ledger mass `v` never lowers the combined cost. Hence the
738non-negativity forcing route is non-vacuous and is satisfied by the intended
739combiner, with the regularity input grounded in `ledgerCost_nonneg` rather than
740analytic continuity. -/
741theorem rclCombiner_postingNonneg :
742 ∀ u v, 0 ≤ u → 0 ≤ v → rclCombiner u 0 ≤ rclCombiner u v := by
743 intro u v hu hv
744 unfold rclCombiner
745 nlinarith [mul_nonneg hu hv, mul_nonneg hu hv]
746
747/-- **Non-vacuity witness for the directional route.** For each fixed first cost
748`u`, the canonical RCL combiner responds to posted mass `v` monotonically in one
749direction: increasing when `u ≥ -1`, decreasing when `u ≤ -1`. This shows the
750`hdir` hypothesis of `primitiveLedgerPosting_directional_forces_rcl` is satisfied
751by the combiner it forces, so the order route is a genuine (non-vacuous) closure,
752unlike the global-monotone and global-nonneg routes which only hold on the
753physical cost cone `u ≥ 0`. -/
754theorem rclCombiner_directional :
755 ∀ u, Monotone (fun v => rclCombiner u v) ∨
756 Antitone (fun v => rclCombiner u v) := by
757 intro u
758 rcases le_or_gt 0 (u + 1) with hu | hu
759 · left
760 intro a b hab
761 unfold rclCombiner
762 nlinarith [mul_nonneg hu (by linarith : (0 : ℝ) ≤ b - a)]
763 · right
764 intro a b hab
765 unfold rclCombiner
766 nlinarith [mul_nonneg (by linarith : (0 : ℝ) ≤ -(u + 1)) (by linarith : (0 : ℝ) ≤ b - a)]
767
768/-- The canonical RCL combiner has ledger-linear response. -/
769theorem rclCombiner_ledgerLinearResponse :
770 LedgerLinearResponse rclCombiner where
771 symmetric := rclCombiner_satisfies_gate.symmetric
772 zeroBoundary := rclCombiner_satisfies_gate.zeroBoundary
773 unitDiagonal := rclCombiner_satisfies_gate.unitDiagonal
774 rightResponse := by
775 intro u v
776 unfold rclCombiner
777 ring
778 free_ledger_additivity := by
779 intro I w Γ Δ
780 exact RecognitionLedgerFloor.ledgerCost_add w Γ Δ
781
782/-- The canonical RCL combiner carries the weaker free-ledger semantics: posted
783increments add, the response is continuous, and the free ledger supplies
784additivity. -/
785theorem rclCombiner_freeLedgerSemantics :
786 FreeLedgerCombinerSemantics rclCombiner where
787 symmetric := rclCombiner_satisfies_gate.symmetric
788 zeroBoundary := rclCombiner_satisfies_gate.zeroBoundary
789 unitDiagonal := rclCombiner_satisfies_gate.unitDiagonal
790 rightPostedAdditive := by
791 intro u v w
792 unfold rclCombiner
793 ring
794 rightContinuous := by
795 intro u
796 unfold rclCombiner
797 continuity
798 free_ledger_additivity := by
799 intro I w Γ Δ
800 exact RecognitionLedgerFloor.ledgerCost_add w Γ Δ
801
802/-- The ledger-linear response target is equivalent to the canonical RCL
803polynomial. This leaves one clean Phase 3 obligation: prove ledger-linear
804response from the free ledger interpretation. -/
805theorem ledgerLinearResponse_iff_rcl (P : ℝ → ℝ → ℝ) :
806 LedgerLinearResponse P ↔ ∀ u v, P u v = rclCombiner u v := by
807 constructor
808 · exact ledgerLinearResponse_forces_rcl P
809 · intro hP
810 refine {
811 symmetric := ?_
812 zeroBoundary := ?_
813 unitDiagonal := ?_
814 rightResponse := ?_
815 free_ledger_additivity := ?_
816 }
817 · intro u v
818 rw [hP u v, hP v u]
819 unfold rclCombiner
820 ring
821 · intro u
822 rw [hP u 0]
823 unfold rclCombiner
824 ring
825 · rw [hP 1 1]
826 unfold rclCombiner
827 norm_num
828 · intro u v
829 rw [hP u v, hP u 1, hP u 0]
830 unfold rclCombiner
831 ring
832 · intro I w Γ Δ
833 exact RecognitionLedgerFloor.ledgerCost_add w Γ Δ
834
835/-- Rational completed ledger posting supplies the full factorization gate. -/
836theorem factorizationGate_of_rationalLedgerPosting
837 (P : ℝ → ℝ → ℝ) (h : RationalLedgerPostingSemantics P) :
838 FactorizationAssociativityGate P :=
839 factorizationGate_of_ledgerLinearResponse P
840 ((rationalLedgerPosting_iff_ledgerLinearResponse P).1 h)
841
842/-- Rational completed ledger posting forces the canonical RCL polynomial. -/
843theorem rationalLedgerPosting_forces_rcl
844 (P : ℝ → ℝ → ℝ) (h : RationalLedgerPostingSemantics P) :
845 ∀ u v, P u v = rclCombiner u v :=
846 ledgerLinearResponse_forces_rcl P
847 ((rationalLedgerPosting_iff_ledgerLinearResponse P).1 h)
848
849/-- Rational completed ledger posting is exactly equivalent to being the
850canonical RCL combiner. -/
851theorem rationalLedgerPosting_iff_rcl (P : ℝ → ℝ → ℝ) :
852 RationalLedgerPostingSemantics P ↔ ∀ u v, P u v = rclCombiner u v := by
853 constructor
854 · exact rationalLedgerPosting_forces_rcl P
855 · intro hP
856 exact (rationalLedgerPosting_iff_ledgerLinearResponse P).2
857 ((ledgerLinearResponse_iff_rcl P).2 hP)
858
859/-- Free-ledger posting semantics and rational completed ledger posting are the
860same completed T5 semantic bridge. -/
861theorem freeLedgerCombinerSemantics_iff_rationalLedgerPosting
862 (P : ℝ → ℝ → ℝ) :
863 FreeLedgerCombinerSemantics P ↔ RationalLedgerPostingSemantics P := by
864 constructor
865 · intro h
866 exact (rationalLedgerPosting_iff_ledgerLinearResponse P).2
867 ((freeLedgerCombinerSemantics_iff_ledgerLinearResponse P).1 h)
868 · intro h
869 exact (freeLedgerCombinerSemantics_iff_ledgerLinearResponse P).2
870 ((rationalLedgerPosting_iff_ledgerLinearResponse P).1 h)
871
872/-- Free-ledger posting semantics is exactly equivalent to being the canonical
873RCL combiner. -/
874theorem freeLedgerCombinerSemantics_iff_rcl (P : ℝ → ℝ → ℝ) :
875 FreeLedgerCombinerSemantics P ↔ ∀ u v, P u v = rclCombiner u v := by
876 constructor
877 · intro h
878 exact ledgerLinearResponse_forces_rcl P
879 ((freeLedgerCombinerSemantics_iff_ledgerLinearResponse P).1 h)
880 · intro hP
881 exact (freeLedgerCombinerSemantics_iff_ledgerLinearResponse P).2
882 ((ledgerLinearResponse_iff_rcl P).2 hP)
883
884end LedgerToFactorization
885end Foundation
886end IndisputableMonolith
887