Verification Rendered

Rendered verification

Verification rendered is the presentation layer of a machine-checked library of formal results. When a proof is verified, it exists as an internal formal object; rendering converts that object into a plain-language summary a person can read. Each rendered claim carries three fields: an identifier, the statement in words or symbols, and a boolean flag saying whether the proof succeeded. This is the difference between a proof existing and a proof being legible.

The module also defines a gate specification, which records the inputs and the symbolic output of a verification check. One example gate takes two uncertainty values, a scaling factor, an optional density, and a constant, and outputs a statistic Z with a pass condition. This is how a rendered page can show not just that a claim was proved, but what data and formula the proof depended on.

The rendered module exports a list of dimensionless results that have been checked with no free parameters, meaning no adjustable constants were fitted to make them work. The list includes a gate inequality, a cone bound, a minimal period of 8 ticks, and a Bianchi identity, among others. Each of these appears in the rendered claims list with its statement and a proved flag set to true.

In practice, this means a reader of the framework's output can see at a glance which results are established and what each one asserts. The rendered form does not add mathematical content; it makes the content inspectable. A claim that fails verification would carry a false flag, and the gate specification shows exactly which inputs would need to change to revisit it.

/-- Rendered summary of a dimensionless claim. -/
structure RenderedClaim where
  id        : String
  statement : String
  proved    : Bool

/-- Rendered gate specification (inputs and symbolic output). -/
structure GateSpec where
  id      : String
  inputs  : List String
  output  : String

/-- Zero-knobs proof bundle export: list of registered dimensionless theorems. -/
@[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

The rendered module itself proves no new results; it only presents results established elsewhere in the library. A proved flag of true does not guarantee the statement is physically meaningful, only that it was formally checked. The gate specification shown is an example, not a complete list of all verification gates in the framework.

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/Rendered.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: