IndisputableMonolith.Verification.KnobsCount

   1import Mathlib
   2
   3/-!
   4# Input Ledger (replaces the former `zero_knobs_policy`)
   5
   6The former `theorem zero_knobs_policy : 0 = 0 := rfl` was removed in the
   72026-07-06 honesty pass: a reflexivity proof of `0 = 0` carries no information
   8about the framework's inputs, and the 2026 internal audit (Thapa, T−2..T5
   9forcing report, §11) correctly identified it as vacuous.
  10
  11What replaces it is the opposite of a vacuous certificate: an explicit,
  12enumerated ledger of every discrete modeling input, convention, and
  13calibration the T−2..T5 layer consumes. "Zero adjustable parameters" is true
  14only in the narrow sense that no CONTINUOUS parameter is fit to data; the
  15discrete structural choices below are real inputs and are named as such.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Verification
  20
  21/-- One named input consumed by the derivation layer. -/
  22structure LedgeredInput where
  23  name : String
  24  kind : String   -- "structural choice" | "convention/normalization" | "bridge hypothesis"
  25  where_used : String
  26deriving Repr, DecidableEq
  27
  28/-- The explicit input ledger for the T−2..T5 layer (audit §11). Each entry is
  29a genuine input: not fit to data, but also not derived from logic alone. -/
  30def inputLedger : List LedgeredInput :=
  31  [ ⟨"observational relation (distinguishability structure)", "structural choice", "T−1 floor"⟩
  32  , ⟨"marked pair / orientation for Boolean projection", "structural choice", "T−1 → Bool coordinate"⟩
  33  , ⟨"Bool indicator model with unit recognition cost", "structural choice", "T0 recognition work"⟩
  34  , ⟨"positive-ratio continuum carrier (SI2, Hölder-type embedding)", "bridge hypothesis", "T4 → T5 comparison surface"⟩
  35  , ⟨"finite polynomial closure / composition law (C6)", "structural choice", "T5 characterization"⟩
  36  , ⟨"bilinear coefficient c = 2 in the combiner", "convention/normalization", "RCL polynomial P(u,v) = 2uv + 2u + 2v"⟩
  37  , ⟨"diagonal normalization P(1,1) = 6", "convention/normalization", "RCL forcing"⟩
  38  , ⟨"log-curvature calibration λ = 1 (C7)", "convention/normalization", "selects J among cosh(λ log x) − 1"⟩
  39  , ⟨"hyperbolic (sign) branch selection", "convention/normalization", "excludes the cosine branch"⟩
  40  ]
  41
  42/-- The ledger is non-empty: the framework HAS inputs, and they are named. -/
  43theorem inputLedger_nonempty : inputLedger ≠ [] := by
  44  simp [inputLedger]
  45
  46/-- Count of ledgered inputs (audit §11 enumeration). -/
  47theorem inputLedger_count : inputLedger.length = 9 := rfl
  48
  49/-- Number of CONTINUOUS parameters fit to empirical data in the T−2..T5
  50proof layer: zero. This narrow claim is the honest survivor of the former
  51"zero knobs" language; the discrete inputs above remain real inputs. -/
  52def fittedContinuousParameterCount : Nat := 0
  53
  54@[simp] theorem no_fitted_continuous_parameters : fittedContinuousParameterCount = 0 := rfl
  55
  56end Verification
  57end IndisputableMonolith
  58