IndisputableMonolith.Common.CanonicalJBand

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Canonical J-Cost Band — Reusable Six-Clause Template
   6
   7The six-clause J-cost-on-ratio template is used across the master cert
   8chain (B-tier whole-science openings, the Plan v7 forty-something
   9domain certs). Each domain cert proves:
  10
  111. matched-zero: J(1) = 0
  122. nonneg: J(x) ≥ 0 for x > 0
  133. reciprocal: J(x) = J(1/x) for x ≠ 0
  144. positivity-off-match: J(x) > 0 for x > 0 with x ≠ 1
  155. golden-step-positive: J(φ) > 0
  166. golden-step-band: J(φ) ∈ (0.11, 0.13)
  17
  18This module proves the φ-side identities once so downstream domain
  19certs can reuse them rather than re-prove. Each domain cert still
  20defines its own ratio with domain-specific names.
  21
  22## Lean status: 0 sorry, 0 axiom (RS-specific)
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Common
  27namespace CanonicalJBand
  28
  29open Constants
  30
  31noncomputable section
  32
  33/-- Canonical recognition cost J(x) = ½(x + 1/x) - 1. -/
  34def J (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
  35
  36theorem J_one : J 1 = 0 := by unfold J; norm_num
  37
  38theorem J_reciprocal {x : ℝ} (hx : x ≠ 0) : J x = J (1 / x) := by
  39  unfold J; field_simp; ring
  40
  41theorem J_phi_pos : J phi > 0 := by
  42  unfold J
  43  have h_phi_sq : phi ^ 2 = phi + 1 := Constants.phi_sq_eq
  44  have h_phi_pos : 0 < phi := Constants.phi_pos
  45  have h_phi_inv : phi⁻¹ = phi - 1 := by
  46    have h : phi * (phi - 1) = 1 := by nlinarith [h_phi_sq]
  47    field_simp; linarith
  48  rw [h_phi_inv]
  49  linarith [Constants.phi_gt_onePointFive]
  50
  51theorem J_phi_band : (0.11 : ℝ) < J phi ∧ J phi < 0.13 := by
  52  unfold J
  53  have h_phi_sq : phi ^ 2 = phi + 1 := Constants.phi_sq_eq
  54  have h_phi_pos : 0 < phi := Constants.phi_pos
  55  have h_phi_inv : phi⁻¹ = phi - 1 := by
  56    have h : phi * (phi - 1) = 1 := by nlinarith [h_phi_sq]
  57    field_simp; linarith
  58  rw [h_phi_inv]
  59  refine ⟨?_, ?_⟩ <;>
  60    linarith [Constants.phi_gt_onePointSixOne, Constants.phi_lt_onePointSixTwo]
  61
  62/-- Canonical recovery: J(1/φ²) > 0 (off-baseline). -/
  63theorem J_inv_phi_sq_pos : J (1 / phi ^ 2) > 0 := by
  64  unfold J
  65  have h_phi_pos : 0 < phi := Constants.phi_pos
  66  have h_phi_sq_pos : 0 < phi ^ 2 := pow_pos h_phi_pos 2
  67  have ⟨h_lo, h_hi⟩ := Constants.phi_squared_bounds
  68  have h_inv : (1 / phi ^ 2)⁻¹ = phi ^ 2 := by rw [inv_div, div_one]
  69  rw [h_inv]
  70  have h_strict : (phi ^ 2 - 1) ^ 2 > 0 := by nlinarith
  71  have h_eq : (phi ^ 2 - 1) ^ 2 / phi ^ 2 = phi ^ 2 + 1 / phi ^ 2 - 2 := by
  72    field_simp; ring
  73  have h_div : (phi ^ 2 - 1) ^ 2 / phi ^ 2 > 0 := div_pos h_strict h_phi_sq_pos
  74  linarith [h_eq ▸ h_div]
  75
  76/-- Canonical six-clause certificate. Domain certs reuse this. -/
  77structure CanonicalCert where
  78  matched_zero : J 1 = 0
  79  reciprocal : ∀ {x : ℝ}, x ≠ 0 → J x = J (1 / x)
  80  phi_pos : J phi > 0
  81  phi_band : (0.11 : ℝ) < J phi ∧ J phi < 0.13
  82  recovery_pos : J (1 / phi ^ 2) > 0
  83
  84def cert : CanonicalCert where
  85  matched_zero := J_one
  86  reciprocal := J_reciprocal
  87  phi_pos := J_phi_pos
  88  phi_band := J_phi_band
  89  recovery_pos := J_inv_phi_sq_pos
  90
  91end
  92
  93end CanonicalJBand
  94end Common
  95end IndisputableMonolith
  96