defect_annular_cost_bounded_inconsistent
A formal proof demonstrates the inconsistency of assuming bounded annular cost for defect sensors carrying nonzero charge. It would be cited when auditing the legacy complex-analysis route to the Riemann hypothesis within Recognition Science. The short tactic proof instantiates a canonical sampled family, extracts the bound, invokes the family-unboundedness result, and obtains a contradiction via comparison of inequalities.
claimLet $S$ be a defect sensor with nonzero charge. Suppose there exists a real number $K$ such that the annular cost of every mesh in the canonical sampled family generated by $S$ is at most $K$. Then this assumption leads to a logical contradiction.
background
The EulerInstantiation module shows that the Euler product of the zeta function satisfies the abstract carrier and sensor interfaces from AnnularCost and CostCoveringBridge. It constructs an instantiation chain from primes through Hilbert-Schmidt norms and logarithmic derivatives to a holomorphic nonvanishing carrier on Re(s) > 1/2, enabling cost-covering axioms. Upstream, cost is the J-cost of a recognition event, while K is the dimensionless bridge ratio defined as phi to the power 1/2. The DefectSensor carries a charge that parametrizes sampled families for cost analysis.
proof idea
The tactic proof first constructs the canonical defect sampled family from the sensor and nonzero-charge hypothesis. It confirms the family inherits the nonzero charge. It then destructures the boundedness hypothesis to extract the constant K. Application of the defect sampled family unboundedness lemma produces an index N at which the cost exceeds K. The final step applies not_lt_of_ge to the bound and the exceeding value to reach falsehood.
why it matters in Recognition Science
This result is invoked directly by rh_from_complex_analysis_axioms, which derives False from the deprecated bounded-cost axiom and is itself marked inconsistent. It thereby closes the legacy analytic path. Preferred routes proceed via UnifiedRH.unified_rh or AnalyticTrace.ZeroFreeCriterion. In the Recognition Science framework it reinforces that bounded annular cost conflicts with the unboundedness of sampled families carrying nonzero charge, consistent with the multiplicative recognizer cost and observer forcing.
scope and limits
- Does not prove the Riemann hypothesis.
- Applies only to sensors with nonzero charge.
- Concerns only the deprecated bounded annular cost hypothesis.
- Does not address the analytic zero-free criterion.
- Limited to annular cost in the sampled trace setting.
formal statement (Lean)
826theorem defect_annular_cost_bounded_inconsistent (sensor : DefectSensor)
827 (hm : sensor.charge ≠ 0)
828 (hbounded : DeprecatedDefectAnnularCostBounded sensor hm) : False := by
proof body
Tactic-mode proof.
829 let fam := canonicalDefectSampledFamily sensor hm
830 have hfam : fam.sensor.charge ≠ 0 := by
831 simpa [fam, canonicalDefectSampledFamily_sensor] using hm
832 obtain ⟨K, hK⟩ := hbounded
833 obtain ⟨N, hN⟩ := defectSampledFamily_unbounded fam hfam K
834 exact not_lt_of_ge (hK N) hN
835
836/-- **RH from the deprecated bounded-cost axiom (legacy path).**
837
838⚠ **INCONSISTENT**: derives `False` from the contradictory axiom
839`defect_annular_cost_bounded`. See `defect_annular_cost_bounded_inconsistent`.
840For the preferred path, see `UnifiedRH.unified_rh` (ontology) or
841`AnalyticTrace.ZeroFreeCriterion` (analytic). -/