theorem proved term proof

`isolated_prime_onehundredtwentyseven`

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

formal statement (Lean)

2867theorem isolated_prime_onehundredtwentyseven : Prime 127 ∧ ¬Prime 125 ∧ ¬Prime 129 := by native_decide

proof body

Term-mode proof.

2868
2869/-- 131 is NOT isolated: 131 - 2 = 129 (composite), but 131 + 2 = 133 = 7 × 19 (composite). -/
2870-- Check: 129 = 3 × 43, 133 = 7 × 19, so 131 IS isolated.

depends on (5)

Lean names referenced from this declaration's body.

is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Prime in IndisputableMonolith.NumberTheory.Primes.Basic decl_use