`IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianNormGate4DAudit`

IndisputableMonolith/Gravity/Analysis/ReggeExactFlatHessianNormGate4DAudit.lean · 16 lines · 1 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianNormGate4D
   2open IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianNormGate4D
   3#print axioms exact_unitFrobenius_ne_frozen_preflight_EH
   4#print axioms frozen_EH_is_discrete_bookkeeping_times_unitF
   5#print axioms continuumEHDiscreteFace_on_unitF
   6#print axioms frozen_EH_is_axisTTPlus_face
   7theorem norm_gate_audit_package :
   8    NormalizationGatePass = true ∧
   9      exactUnitFrobeniusTTCoefficient ≠ frozenPreflightEHCoefficient ∧
  10        frozenPreflightEHCoefficient =
  11          discreteBookkeepingFactor * exactUnitFrobeniusTTCoefficient ∧
  12            continuumEHDiscreteFace (1 : ℝ) = frozenPreflightEHCoefficient :=
  13  ⟨normalizationGatePass_true, exact_unitFrobenius_ne_frozen_preflight_EH,
  14    frozen_EH_is_discrete_bookkeeping_times_unitF, continuumEHDiscreteFace_on_unitF⟩
  15#print axioms norm_gate_audit_package
  16

source mirrored from github.com/jonwashburn/shape-of-logic