Gravity Track1 Bcstructural Track1 Bcstructural Cert

The structural witness

Track1BCStructuralCert is a formal object in the Recognition Science framework's machine-checked library of formal theorems. It bundles together two structural claims about gravity, each stated under a named hypothesis rather than as a finished proof. The certificate exists to show that the framework's master theorem about gravity has a consistent input: the two pieces can be stated and inhabited without contradiction.

The first piece concerns the Regge action, a way of writing gravity on a lattice of discrete simplices, and its relation to the Einstein-Hilbert action, the standard continuous formulation. The structural claim says that if a geometric residual bound holds, then as the lattice spacing shrinks to zero, the difference between the two actions tends to zero. The second piece concerns the contracted second Bianchi identity, a conservation law in gravity, on the discrete lattice. The structural claim says that if the Schläfli identity holds at every vertex, then the discrete Bianchi identity holds at every vertex.

Both claims are proved in the library, but only in their structural form. The witnesses used are canonical flat-substrate examples: for the Regge-EH convergence, both actions are zero, so the difference is trivially zero; for the discrete Bianchi, a trivial unit-type triangulation satisfies the Schläfli identity. These witnesses show the structural statements are non-vacuous, but they do not supply the actual geometric residual estimate or the Schläfli identity proof for a physical triangulation. Those unconditional proofs remain future work.

The certificate itself is a structure that packages the two structural claims and the master theorem hypothesis witness. The library proves the certificate is inhabited, meaning such a package exists. This is a genuine theorem, but its content is deliberately limited: it certifies that the structural statements hold, not that the full unconditional claims hold.

In plain terms, the certificate is a scaffolding. It says: if these geometric conditions are met, then these consequences follow, and here is a trivial example showing the conditions are not empty. It does not say the conditions are met for actual spacetime. The distinction is load-bearing for anyone reading the framework's gravity claims.

structure Track1BCStructuralCert where
  regge_eh_canonical : regge_eh_continuum_structural_prop
  discrete_bianchi_canonical : discrete_bianchi_structural_prop
  combined_holds :
    regge_eh_continuum_structural_prop ∧ discrete_bianchi_structural_prop
  master_hypothesis_witness :
    Gravity.MasterTheorem.RegEHContinuumAndBianchi

/-- The structural Regge-EH convergence Prop: for any sequence of
spacings tending to zero, the absolute difference of the abstract
Regge and EH actions tends to zero. For the flat substrate canonical
witness, both are zero, so the difference is zero. -/
def regge_eh_continuum_structural_prop : Prop :=
  ∀ (spacing : ℝ), abstract_regge_action spacing = abstract_eh_action spacing

/-- The structural discrete Bianchi Prop: there exists a Schläfli-satisfying
Regge triangulation, witnessing the contracted second Bianchi identity
at every vertex (via Session 98's `Geometry.DiscreteBianchi`). -/
def discrete_bianchi_structural_prop : Prop :=
  ∃ (V B : Type) (_ : Fintype B),
    Nonempty (Geometry.DiscreteBianchi.SchlafliReggeData V B)

theorem regge_eh_continuum_canonical_witness :
    regge_eh_continuum_structural_prop := by
  intro spacing
  unfold abstract_regge_action abstract_eh_action
  rfl

theorem discrete_bianchi_canonical_witness :
    discrete_bianchi_structural_prop :=
  ⟨Unit, Unit, inferInstance,
   Geometry.DiscreteBianchi.SchlafliReggeData_inhabited Unit Unit⟩

theorem track1BCStructuralCert_inhabited :
    Nonempty Track1BCStructuralCert :=
  ⟨track1BCStructuralCert⟩

What this page does not claim

The unconditional Regge-EH convergence for physical triangulations is not proved. The unconditional discrete Bianchi identity for physical triangulations is not proved. The certificate does not claim that actual spacetime satisfies the named geometric hypotheses.

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/Gravity/Track1BCStructural.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: