Encyclopedia Gravity Gravity Master Theorem Non Circularity Audit Cost Uniqueness Clause Is Carried

ARTICLE 3 claims 3 theorems

Gravity Master Theorem Non Circularity Audit Cost Uniqueness Clause Is Carried

A formal audit shows the gravity master theorem's cost-uniqueness clause is a real, independently proven statement, not a placeholder.

Verify this page

What the cost clause carries

In a machine-checked library of formal theorems, a large theorem is often built from smaller parts. A referee worried that some of those parts might be empty shells: statements that look meaningful but are actually just the proposition "true," which carries no information. The audit answers that worry for the gravity master theorem by examining each clause. One clause, cost uniqueness, states that a certain cost function is the only one satisfying its defining conditions. The audit's theorem costUniqueness_clause_is_carried shows that this clause is exactly equal to a separately named proposition, CostUniqueness_carried_prop, and a companion theorem proves that proposition holds.

This matters because the master theorem's conclusion is only as strong as its parts. If a clause were a placeholder, the master theorem would not actually prove that clause. The audit shows the cost-uniqueness clause is not a placeholder. It is a genuine, independently established result that the master theorem carries along. The audit also provides a standalone proof, costUniqueness_clause_holds, which does not assume the master theorem itself. So the clause is both real and non-circular: it does not secretly depend on the conclusion it is supposed to support.

The audit classifies all fifteen clauses of the master theorem. Zero are placeholders. Nine are certificates, meaning they are witnessed by explicit constructions. Six are general statements with substantive proofs. The cost-uniqueness clause falls into the substantive group. This classification is itself a proved theorem. The audit's final certificate assembles all the clauses and confirms that none of them is the master conclusion itself.

What the declaration does not claim is just as important. It does not prove the cost uniqueness theorem from scratch; that proof lives elsewhere in the library. It does not say the cost-uniqueness result is physically true in the world. It only says that the master theorem's statement of cost uniqueness is identical to a named, independently proven proposition, and that this proposition holds. The audit is about the logical structure of the library, not about physics.

THEOREM costUniqueness_clause_is_carried · costUniqueness_clause_holds · IndisputableMonolith/Gravity/MasterTheoremNonCircularityAudit.lean
costUniqueness_clause_is_carried · IndisputableMonolith/Gravity/MasterTheoremNonCircularityAudit.lean:72 
/-- The cost-uniqueness master clause now carries the universal J-cost
uniqueness proposition. -/
theorem costUniqueness_clause_is_carried :
    MasterTheorem.CostUniqueness =
      MasterTheorem.CostUniqueness_carried_prop := rfl
costUniqueness_clause_holds · IndisputableMonolith/Gravity/MasterTheoremNonCircularityAudit.lean:78 
/-- The carried cost-uniqueness clause holds by
`Cost.FunctionalEquation.law_of_logic_forces_jcost`. -/
theorem costUniqueness_clause_holds : MasterTheorem.CostUniqueness :=
  MasterTheorem.CostUniqueness_proven
THEOREM masterClauseClassification_total · placeholderClauseCount · inhabitedCertClauseCount · witnessFieldClauseCount · IndisputableMonolith/Gravity/MasterTheoremNonCircularityAudit.lean
masterClauseClassification_total · IndisputableMonolith/Gravity/MasterTheoremNonCircularityAudit.lean:263 
theorem masterClauseClassification_total :
    masterClauseClassification.placeholder +
      masterClauseClassification.inhabitedCert +
      masterClauseClassification.witnessField = 15 := by decide
placeholderClauseCount · IndisputableMonolith/Gravity/MasterTheoremNonCircularityAudit.lean:93 
/-- Count of `True` placeholder clauses in the master conjunction after M3. -/
def placeholderClauseCount : ℕ := 0
inhabitedCertClauseCount · IndisputableMonolith/Gravity/MasterTheoremNonCircularityAudit.lean:172 
/-- Count of carried/certificate closed clauses (after M3; after M4 all six
certificate clauses additionally carry their propositional content). -/
def inhabitedCertClauseCount : ℕ := 9
witnessFieldClauseCount · IndisputableMonolith/Gravity/MasterTheoremNonCircularityAudit.lean:224 
/-- Count of witness-field clauses (D2×2, D3, D4, D5×2). -/
def witnessFieldClauseCount : ℕ := 6
THEOREM master_theorem_non_circularity_certificate · IndisputableMonolith/Gravity/MasterTheoremNonCircularityAudit.lean
master_theorem_non_circularity_certificate · IndisputableMonolith/Gravity/MasterTheoremNonCircularityAudit.lean:268 
/-- **NON-CIRCULARITY CERTIFICATE (one statement).**

1. The T0-T8 clause carries the T0-through-T8 theorem-surface conjunction.
2. The cost-uniqueness clause carries the universal J-cost uniqueness theorem.
3. The BMV-positivity clause carries the pure two-qubit entropy theorem.
4. The six closed certificate clauses hold by certificate inhabitation.
5. The five witness inputs hold unconditionally (no master clause assumed).
6. The D4 Page field is non-vacuous (strict rise to an interior peak).
7. Therefore the unconditional master theorem holds, assembled from
   independently-proved, concretely-named, non-self-referential propositions.

A referee can read off each field's definition from §1–§3 and confirm none
is `RSQuantumGravityMaster`; the circularity objection (F1) is discharged at
the granularity of individual fields. -/
theorem master_theorem_non_circularity_certificate :
    (MasterTheorem.T0_T8_holds = MasterTheorem.T0_T8_carried_prop ∧
     MasterTheorem.T0_T8_holds ∧
     MasterTheorem.CostUniqueness = MasterTheorem.CostUniqueness_carried_prop ∧
     MasterTheorem.CostUniqueness ∧
     MasterTheorem.bmv_positive_unconditional =
       MasterTheorem.bmv_positive_unconditional_carried_prop ∧
     MasterTheorem.bmv_positive_unconditional) ∧
    (MasterTheorem.Lorentzian_1_3 ∧
     MasterTheorem.hawking_temperature_SI ∧
     MasterTheorem.c_RS_observable_distinct ∧
     MasterTheorem.omega_lambda_from_phi ∧
     MasterTheorem.rs_qnm_distinct_LQG_string ∧
     MasterTheorem.gravity_sector_zero_free_parameters) ∧
    (canonicalRegEHContinuumAndBianchiWitness.regge_to_einstein_hilbert_continuum ∧
     canonicalRegEHContinuumAndBianchiWitness.discrete_bianchi_contracted ∧
     canonicalAmplitudeLinearForcedWitness.amplitude_linear_forced_unconditional ∧
     canonicalPageCurveDerivedWitness.page_curve_derived ∧
     canonicalPTADistinctWitness.rs_pta_distinct_inflation ∧
     canonicalStrongFieldDistinctWitness.rs_strong_field_distinct_GR_only) ∧
    MasterTheorem.RSQuantumGravityMaster
      canonicalRegEHContinuumAndBianchiWitness
      canonicalAmplitudeLinearForcedWitness
      canonicalPageCurveDerivedWitness
      canonicalPTADistinctWitness
      canonicalStrongFieldDistinctWitness :=
  ⟨⟨t0t8_clause_is_complete_forcing_chain,
     carried_clauses_hold.1,
     costUniqueness_clause_is_carried,
     carried_clauses_hold.2.1,
     bmv_clause_is_carried,
     carried_clauses_hold.2.2⟩,
   closed_certs_hold,
   all_witness_fields_hold,
   rs_quantum_gravity_master_unconditional⟩

What this page does not claim

It does not prove the cost uniqueness theorem from scratch. It does not assert that the cost uniqueness result is physically true in the world. It does not say that the master theorem is a valid physical theory, only that its logical structure is non-circular.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND