theorem proved term proof

`larger_charge_larger_span`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 128theorem larger_charge_larger_span :
 129    Q_tilde_up > Q_tilde_down ∧
 130    (13 + 11 : ℕ) > (6 + 8) := by

proof body

Term-mode proof.

 131  unfold Q_tilde_up Q_tilde_down
 132  constructor <;> omega
 133
 134/-! ## Main Theorem: SDGT is Forced -/
 135
 136/-- The complete forcing result: given the four step values and the
 137    partition + charge constraints, the SDGT assignment is unique. -/

depends on (9)

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
complete in IndisputableMonolith.Complexity.SAT.Backprop decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
Q_tilde_down in IndisputableMonolith.Masses.SDGTForcing decl_use
Q_tilde_up in IndisputableMonolith.Masses.SDGTForcing decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use