Pith. sign in

IndisputableMonolith.Skeleton.Cost

IndisputableMonolith/Skeleton/Cost.lean · 37 lines · 0 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending

   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

source mirrored from github.com/jonwashburn/shape-of-logic