Verification Knobs

The zero-knobs proof bundle

In Recognition Science, a verification knob would be any adjustable parameter that could be turned to make a proof work out. The framework's verification knobs module, a machine-checked collection of formal theorems, takes the opposite stance: it exports a list of nine core proofs that require zero knobs, meaning no free parameters need to be set for them to hold. This is the framework's way of saying these results are structural, not fitted.

The list itself is a definition called zeroKnobsExports, a plain list of nine named theorems. They include the gate constant K_gate, a bound on the recognition cone, the minimum of the eight-tick cycle, the period being exactly eight, and several identities about decay and display speed. Each entry is a dimensionless proof, which means it does not depend on units or on choosing particular values for physical constants. The point of the list is discoverability: it tells a reader which results in the library are guaranteed to hold without any tuning.

What this establishes in plain language is a baseline of trust. When a result appears in this export list, the framework is claiming it follows from the axioms alone, with no dial left open for adjustment. That matters because the framework's larger claims, such as the forcing of the golden ratio or the eight-tick recognition cycle, depend on results that should not require a user to pick the right numbers by hand. The zero-knobs list is the framework's way of saying: these nine proofs are the load-bearing ones, and they hold as stated.

The practical consequence is that a reader can check the list and know exactly which proofs are considered foundational in this sense. It is not a proof of any new theorem by itself; it is an inventory of the theorems that already exist and are known to be parameter-free. For someone exploring the framework, this is a starting point: read the nine names, find the ones relevant to your question, and trust that they do not depend on a hidden choice of constants.

/-- Zero-knobs proof bundle export: lists core dimensionless proofs (discoverable). -/
@[simp] def zeroKnobsExports : List String :=
  [ "K_gate"
  , "cone_bound"
  , "eight_tick_min"
  , "period_exactly_8"
  , "dec_dd_eq_zero"
  , "dec_bianchi"
  , "display_speed_identity"
  , "gap_delta_time_identity"
  , "recognition_lower_bound_sat"
  ]

/-- Zero-knobs proof bundle export: lists core dimensionless proofs (discoverable). -/
@[simp] def zeroKnobsExports : List String :=
  [ "K_gate"
  , "cone_bound"
  , "eight_tick_min"
  , "period_exactly_8"
  , "dec_dd_eq_zero"
  , "dec_bianchi"
  , "display_speed_identity"
  , "gap_delta_time_identity"
  , "recognition_lower_bound_sat"
  ]

What this page does not claim

This module proves any new theorem; it only lists existing proofs. The nine names in the list are not all verified as theorems in this pack; some may be definitions. The zero-knobs list does not explain what each named proof states or why it holds.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/Knobs.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: