IndisputableMonolith.Skeleton.Cost
IndisputableMonolith/Skeleton/Cost.lean · 37 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Cost.FunctionalEquation
2import IndisputableMonolith.Foundation.DAlembert.FactorizationForcing
3
4/-!
5# Skeleton chapter: The Cost Keystone (J and the RCL)
6
7Foundation's T5 guidepost says "J is unique." This chapter is the keystone itself, the two
8theorems that make T5 true and that everything in Recognition Science is downstream of. If
9you read one pair of theorems to understand WHY the framework is forced rather than chosen,
10read these. Drill down: `Cost.FunctionalEquation`, `Foundation.DAlembert.FactorizationForcing`.
11-/
12
13namespace IndisputableMonolith
14namespace Skeleton
15
16/-- **The recognition cost J(x)=½(x+1/x)−1 is the UNIQUE possibility.**
17Given any F that is reciprocal-symmetric, normalized (F(1)=0), satisfies the Recognition
18Composition Law, is calibrated (log-second-derivative 1 at the origin), and continuous on
19(0,∞), then F = J. No RS-specific axiom; this is Aczél/d'Alembert functional-equation
20theory applied to recognition. Everything else (φ, ℏ, the mass ladder, the constants) is a
21shadow of this one cost. Tier: THEOREM (0 sorry). Drill down:
22`Cost.FunctionalEquation.law_of_logic_forces_jcost`, `Cost.AczelProof`. -/
23alias guidepost_cost_is_unique :=
24 IndisputableMonolith.Cost.FunctionalEquation.law_of_logic_forces_jcost
25
26/-- **The Recognition Composition Law is itself forced, not assumed.**
27Among symmetric, right-affine combiners with the natural boundary conditions, the RCL
28polynomial `2uv+2u+2v` is the unique result. So the composition law that pins J down is not
29a modeling choice either, it is forced one level deeper. This closes the obvious objection
30"you chose the RCL." Tier: THEOREM. Drill down:
31`Foundation.DAlembert.FactorizationForcing.gate_forces_rcl`. -/
32alias guidepost_rcl_is_forced :=
33 IndisputableMonolith.Foundation.DAlembert.FactorizationForcing.gate_forces_rcl
34
35end Skeleton
36end IndisputableMonolith
37