7 Non-vacuity of the assumption surface
There is an instance ToyTrivial : ClassicalInputs, with every field discharged in a toy world (\(S = \varnothing \), \(D_E\) a single point, \(L_p = T^2\)) and no incomplete proof. So ClassicalInputs is consistent and the theorems are not vacuously true.
Every interface layer is instantiated concretely under Toy/, and the tie-equations of PrimeData are discharged by computation. #print axioms ToyTrivial shows only propext, Classical.choice and Quot.sound.
ClassicalInputs does not by itself entail \(\mathrm{III}(E/\mathbb {Q})[p^\infty ] = 0\): there is a second instance ToySha : ClassicalInputs at which \(\mathrm{III}[p^\infty ] \ne 0\), \(\mu _{\mathrm{an}} \ne 0\) and \(\lambda _{\mathrm{an}} \ne 2\) at every split prime, and at which the computed \(5\)-adic expansion of \(c_2(5)\) is false. The unit condition, not the interface, is what excludes this world.
toySha_conclusions_fail shows the three conclusions fail at every split prime of the world ToySha; interface_does_not_force_sha_trivial is the non-entailment statement. toySha_fails_c2_5_certificate shows that in this world \(\mathrm{coeff}_2\, L_p = p\), so the leading \(5\)-adic digit of \(c_2(5)\) is \(0\), whereas the computed value for \(y^2 = x^3 - 56x\) has leading digit \(1\). The seven \(5\)-adic digits used there are this project’s own computation, cross-checked by two implementations; the paper does not display them.