IndisputableMonolith.NumberTheory.AnalyticTrace

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4import IndisputableMonolith.NumberTheory.AnnularCost
   5import IndisputableMonolith.NumberTheory.CostCoveringBridge
   6import IndisputableMonolith.NumberTheory.EulerCarrierComplex
   7import IndisputableMonolith.NumberTheory.ContourWinding
   8import IndisputableMonolith.NumberTheory.SampledTrace
   9import IndisputableMonolith.NumberTheory.EulerInstantiation
  10import IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
  11import IndisputableMonolith.NumberTheory.ArgumentPrincipleProved
  12import IndisputableMonolith.NumberTheory.HonestPhaseBudgetBridge
  13import IndisputableMonolith.NumberTheory.ZeroCompositionInterface
  14import IndisputableMonolith.Unification.UnifiedRH
  15
  16/-!
  17# Analytic Trace Interface — Axiom-Free Version
  18
  19Assembles the full RH bridge from the analytic trace infrastructure.
  20
  21## Former axioms — now eliminated
  22
  23The previous version of this module contained two axioms:
  24* `zeroWindingOfHolNonvanishing` — replaced by `EulerCarrierComplex.contourWinding`
  25  (which derives zero winding from holomorphy + nonvanishing)
  26* `argument_principle_forces_charge_zero` — replaced by the floor-coverage
  27  iff theorem `eulerSampledFloorCovered_iff_charge_zero`
  28
  29## Current axiom status
  30
  31Two routes to RH exist:
  32
  331. **Ontology route** (`UnifiedRH.lean`): external bridge hypothesis
  34   `EulerBoundaryBridgeAssumption`.
  35   Preferred path. See `UnifiedRH.unified_rh`.
  36
  372. **Pure analytic route**: targets a `ZeroFreeCriterion` from honest ζ⁻¹ phase
  38   data. `defect_annular_cost_bounded` in `EulerInstantiation.lean` remains as
  39   a deprecated RH-equivalent boundary marker.
  40
  41## This module's contribution
  42
  43Carrier-side infrastructure (axiom-free):
  44* The sampled Euler package has budget 0 (from zero-winding cert)
  45* Floor coverage holds iff charge = 0 (proved, not assumed)
  46* Any sensor with charge ≠ 0 cannot be floor-covered (proved)
  47* Direct RH from `ZeroFreeCriterion` (analytic route target)
  48-/
  49
  50namespace IndisputableMonolith
  51namespace NumberTheory
  52namespace AnalyticTrace
  53
  54open Real Constants Cost
  55open EulerCarrierComplex ContourWinding SampledTrace
  56
  57/-! ### §1. The sampled Euler package -/
  58
  59/-- The sampled Euler `CostCoveringPackage` for any σ₀ > 1/2.
  60Built from the zero-winding certificate, not from a synthetic zero-charge trace. -/
  61noncomputable def eulerSampledCoveringPackage (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
  62    CostCoveringPackage :=
  63  eulerSampledPackage σ₀ hσ
  64
  65/-! ### §2. Floor coverage iff charge = 0 (proved, not axiomatized) -/
  66
  67/-- The defect topological floor is covered by the sampled Euler package
  68if and only if the sensor charge is 0. -/
  69theorem floorCovered_iff_charge_zero (σ₀ : ℝ) (hσ : 1/2 < σ₀)
  70    (sensor : DefectSensor) :
  71    DefectTopologicalFloorCovered (eulerSampledCoveringPackage σ₀ hσ) sensor ↔
  72      sensor.charge = 0 :=
  73  eulerSampledFloorCovered_iff_charge_zero σ₀ hσ sensor
  74
  75/-! ### §3. Carrier-side RH obstruction (no axioms) -/
  76
  77/-- A DefectSensor with charge ≠ 0 can never have its floor covered by
  78the sampled Euler package. The defect floor grows as m² log N while the
  79carrier budget is 0. -/
  80theorem carrier_side_obstruction (sensor : DefectSensor) (hm : sensor.charge ≠ 0) :
  81    ¬ DefectTopologicalFloorCovered
  82        (eulerSampledCoveringPackage sensor.realPart sensor.in_strip.1) sensor :=
  83  not_DefectTopologicalFloorCovered _ sensor hm
  84
  85/-- If floor coverage holds for the sampled package, the charge must be 0. -/
  86theorem charge_zero_of_covered (σ₀ : ℝ) (hσ : 1/2 < σ₀)
  87    (sensor : DefectSensor)
  88    (hcover : DefectTopologicalFloorCovered (eulerSampledCoveringPackage σ₀ hσ) sensor) :
  89    sensor.charge = 0 :=
  90  (floorCovered_iff_charge_zero σ₀ hσ sensor).mp hcover
  91
  92/-! ### §4. Zero-free criterion (analytic route target) -/
  93
  94/-- The zero-free criterion for the pure analytic route.
  95
  96This structure packages the honest analytic target: witnessed ζ⁻¹ defect data
  97in the strip gives an honest phase-family package, and analytic estimates then
  98force the corresponding defect charge to vanish.
  99
 100**Field status (April 2026):**
 101- `logDeriv_bounded_on_strip`: **PROVED** (`carrierDerivBound_pos`).
 102- `carrier_nonvanishing_on_strip`: **PROVED** (`carrier_nonvanishing`).
 103- `honest_phase_family`: **PROVED** via `honest_argument_principle_phase_family`,
 104  now using `zetaDerivedPhaseFamily` (genuine phase data from meromorphic
 105  factorization) rather than the former `trivialDefectPhaseFamily` scaffold.
 106- `charge_zero_of_honest_phase`: **NARROWED TARGET**. Honest phase data now
 107  comes with a canonical perturbation witness, and the present sampled family
 108  sits exactly on the topological floor (`annularExcess = 0`). The remaining
 109  content is to upgrade the honest sampled family to bounded total cost / floor
 110  coverage, forcing charge = 0.
 111
 112This replaces the deprecated `defect_annular_cost_bounded` as the proper
 113analytic-route target. -/
 114structure ZeroFreeCriterion where
 115  logDeriv_bounded_on_strip :
 116    ∀ σ, 1/2 < σ → 0 < carrierDerivBound σ
 117  carrier_nonvanishing_on_strip :
 118    ∀ σ, 1/2 < σ → carrierValue σ ≠ 0
 119  honest_phase_family :
 120    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 →
 121      ∃ zfd : ZetaPhaseFamilyData,
 122        zfd.sensor = sensor.toDefectSensor ∧
 123          zfd.phaseFamily.sensor = sensor.toDefectSensor
 124  charge_zero_of_honest_phase :
 125    ∀ (sensor : WitnessedDefectSensor),
 126      (∃ zfd : ZetaPhaseFamilyData,
 127        zfd.sensor = sensor.toDefectSensor ∧
 128          zfd.phaseFamily.sensor = sensor.toDefectSensor) →
 129        sensor.charge = 0
 130
 131/-- A `ZeroFreeCriterion` gives the RH directly. -/
 132theorem rh_from_zero_free_criterion (zfc : ZeroFreeCriterion) :
 133    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False := by
 134  intro sensor hm
 135  obtain ⟨zfd, hzfd, hfamily⟩ := zfc.honest_phase_family sensor hm
 136  have hzero : sensor.charge = 0 :=
 137    zfc.charge_zero_of_honest_phase sensor ⟨zfd, hzfd, hfamily⟩
 138  exact hm hzero
 139
 140/-! ### §4b. Vector C insertion point -/
 141
 142/-- A minimal Euler/Hadamard-side bridge for the honest analytic route.
 143
 144The current code already supplies perturbation control, and the present honest
 145sampled family has exact zero excess. The remaining bridge is to show that the
 146honest sampled family also has bounded total annular cost. Once that is known,
 147the general defect-cost theorem forces zero charge immediately. -/
 148structure HonestPhaseCostBridge where
 149  cost_bounded_of_honest_phase :
 150    ∀ (sensor : WitnessedDefectSensor) (zfd : ZetaPhaseFamilyData),
 151      zfd.sensor = sensor.toDefectSensor →
 152        RealizedDefectAnnularCostBounded (zfd.phaseFamily.toSampledFamily)
 153
 154/-- Any honest-phase cost bridge discharges the sole remaining analytic
 155charge-zero target. -/
 156theorem charge_zero_of_honest_phase_of_costBridge
 157    (hb : HonestPhaseCostBridge)
 158    (sensor : WitnessedDefectSensor)
 159    (hzfd : ∃ zfd : ZetaPhaseFamilyData,
 160      zfd.sensor = sensor.toDefectSensor ∧
 161        zfd.phaseFamily.sensor = sensor.toDefectSensor) :
 162    sensor.charge = 0 := by
 163  rcases hzfd with ⟨zfd, hzsensor, _hzfamily⟩
 164  have hcost : RealizedDefectAnnularCostBounded (zfd.phaseFamily.toSampledFamily) :=
 165    hb.cost_bounded_of_honest_phase sensor zfd hzsensor
 166  have hzero_sensor : zfd.sensor.charge = 0 :=
 167    honestPhaseFamily_charge_zero_of_costBounded zfd hcost
 168  have hzero_base : sensor.toDefectSensor.charge = 0 := by
 169    simpa [hzsensor] using hzero_sensor
 170  simpa using hzero_base
 171
 172/-- Therefore a bounded-cost bridge for honest phase data already yields a full
 173analytic `ZeroFreeCriterion`, independently of Vector C. -/
 174noncomputable def zeroFreeCriterion_of_honestPhaseCostBridge
 175    (hb : HonestPhaseCostBridge) :
 176    ZeroFreeCriterion where
 177  logDeriv_bounded_on_strip := fun _ hσ => carrierDerivBound_pos hσ
 178  carrier_nonvanishing_on_strip := fun _ hσ => carrier_nonvanishing hσ
 179  honest_phase_family := honest_argument_principle_phase_family
 180  charge_zero_of_honest_phase := charge_zero_of_honest_phase_of_costBridge hb
 181
 182/-- Consequently any honest-phase bounded-cost bridge proves RH through the
 183existing analytic route. -/
 184theorem direct_rh_from_honestPhaseCostBridge (hb : HonestPhaseCostBridge) :
 185    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
 186  rh_from_zero_free_criterion (zeroFreeCriterion_of_honestPhaseCostBridge hb)
 187
 188/-! ### §4b'. Route C bottleneck — exact current analytic state -/
 189
 190/-- Honest zeta phase data already has bounded excess, but bounded total cost
 191is equivalent to zero charge.  This records the exact Route C bottleneck:
 192the perturbative/excess estimate is complete; the missing analytic content is
 193the upgrade from bounded excess to zero charge (or an equivalent admissibility
 194principle). -/
 195theorem honestPhase_routeC_bottleneck (zfd : ZetaPhaseFamilyData) :
 196    RealizedDefectAnnularExcessBounded (zfd.phaseFamily.toSampledFamily) ∧
 197      (RealizedDefectAnnularCostBounded (zfd.phaseFamily.toSampledFamily) ↔
 198        zfd.sensor.charge = 0) :=
 199  ⟨honestPhaseFamily_excess_bounded zfd,
 200    honestPhaseFamily_cost_bounded_iff_charge_zero zfd⟩
 201
 202/-- A direct charge-zero bridge for honest zeta phase data.  This is weaker
 203and cleaner than asking for bounded total cost: it states exactly the charge
 204conclusion needed by the analytic route. -/
 205structure HonestPhaseChargeZeroBridge where
 206  charge_zero_of_honest_phase :
 207    ∀ zfd : ZetaPhaseFamilyData, zfd.sensor.charge = 0
 208
 209/-- A direct honest-phase charge-zero bridge discharges the `ZeroFreeCriterion`
 210charge-zero field. -/
 211theorem charge_zero_of_honest_phase_of_chargeZeroBridge
 212    (hb : HonestPhaseChargeZeroBridge)
 213    (sensor : WitnessedDefectSensor)
 214    (hzfd : ∃ zfd : ZetaPhaseFamilyData,
 215      zfd.sensor = sensor.toDefectSensor ∧
 216        zfd.phaseFamily.sensor = sensor.toDefectSensor) :
 217    sensor.charge = 0 := by
 218  rcases hzfd with ⟨zfd, hzsensor, _hzfamily⟩
 219  have hz : zfd.sensor.charge = 0 := hb.charge_zero_of_honest_phase zfd
 220  have hs : sensor.toDefectSensor.charge = 0 := by
 221    simpa [hzsensor] using hz
 222  simpa using hs
 223
 224/-- A direct charge-zero bridge gives a full `ZeroFreeCriterion`. -/
 225noncomputable def zeroFreeCriterion_of_honestPhaseChargeZeroBridge
 226    (hb : HonestPhaseChargeZeroBridge) :
 227    ZeroFreeCriterion where
 228  logDeriv_bounded_on_strip := fun _ hσ => carrierDerivBound_pos hσ
 229  carrier_nonvanishing_on_strip := fun _ hσ => carrier_nonvanishing hσ
 230  honest_phase_family := honest_argument_principle_phase_family
 231  charge_zero_of_honest_phase :=
 232    charge_zero_of_honest_phase_of_chargeZeroBridge hb
 233
 234/-- Any direct honest-phase charge-zero bridge proves the analytic RH core. -/
 235theorem direct_rh_from_honestPhaseChargeZeroBridge
 236    (hb : HonestPhaseChargeZeroBridge) :
 237    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
 238  rh_from_zero_free_criterion
 239    (zeroFreeCriterion_of_honestPhaseChargeZeroBridge hb)
 240
 241/-! ### §4c. Vector C insertion point -/
 242
 243/-- A successful Vector C bridge is exactly a mechanism that turns honest
 244zeta-derived phase data into a `ZeroCompositionWitness` for the witnessed zero.
 245
 246Once this structure is instantiated, the existing analytic RH route closes
 247without any further changes to the `ZeroFreeCriterion` contract. -/
 248structure VectorCChargeZeroBridge where
 249  witness_of_honest_phase :
 250    ∀ (sensor : WitnessedDefectSensor),
 251      (∃ zfd : ZetaPhaseFamilyData,
 252        zfd.sensor = sensor.toDefectSensor ∧
 253          zfd.phaseFamily.sensor = sensor.toDefectSensor) →
 254        ZeroCompositionWitness sensor.rho
 255
 256/-- Any Vector C bridge discharges the sole open analytic target:
 257`charge_zero_of_honest_phase`. -/
 258theorem charge_zero_of_honest_phase_of_vectorC
 259    (vc : VectorCChargeZeroBridge)
 260    (sensor : WitnessedDefectSensor)
 261    (hzfd : ∃ zfd : ZetaPhaseFamilyData,
 262      zfd.sensor = sensor.toDefectSensor ∧
 263        zfd.phaseFamily.sensor = sensor.toDefectSensor) :
 264    sensor.charge = 0 := by
 265  have hline : OnCriticalLine sensor.rho :=
 266    zeroCompositionWitness_forces_on_critical_line
 267      (vc.witness_of_honest_phase sensor hzfd)
 268  have hcontr : False := by
 269    have hstrip : 1 / 2 < sensor.rho.re := sensor.in_strip.1
 270    have hre : sensor.rho.re = 1 / 2 := hline
 271    linarith
 272  exact False.elim hcontr
 273
 274/-- A successful Vector C bridge upgrades the proved Euler-carrier and honest
 275phase-family infrastructure into a complete `ZeroFreeCriterion`. -/
 276noncomputable def zeroFreeCriterion_of_vectorC
 277    (vc : VectorCChargeZeroBridge) :
 278    ZeroFreeCriterion where
 279  logDeriv_bounded_on_strip := fun _ hσ => carrierDerivBound_pos hσ
 280  carrier_nonvanishing_on_strip := fun _ hσ => carrier_nonvanishing hσ
 281  honest_phase_family := honest_argument_principle_phase_family
 282  charge_zero_of_honest_phase := charge_zero_of_honest_phase_of_vectorC vc
 283
 284/-- Therefore any successful Vector C bridge proves RH via the existing
 285analytic route. -/
 286theorem direct_rh_from_vectorC_bridge (vc : VectorCChargeZeroBridge) :
 287    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
 288  rh_from_zero_free_criterion (zeroFreeCriterion_of_vectorC vc)
 289
 290/-! ### §5. Full RH from complex-analysis axioms (legacy path)
 291
 292**WARNING**: The theorems below depend on the deprecated axiom
 293`defect_annular_cost_bounded` which is logically inconsistent with proved
 294results. They are retained only as the legacy reference path. The preferred
 295routes are:
 296- Ontology: `UnifiedRH.unified_rh` (external bridge hypothesis)
 297- Analytic: `ZeroFreeCriterion` via honest ζ⁻¹ phase data (§4 above) -/
 298
 299/-- **The Riemann Hypothesis (legacy analytic route).**
 300
 301⚠ DEPRECATED: depends on `defect_annular_cost_bounded`.
 302For the preferred route, see `UnifiedRH.unified_rh` (ontology) or
 303`direct_rh_from_zero_free_criterion` (analytic). -/
 304theorem analytic_rh (sensor : DefectSensor) (hm : sensor.charge ≠ 0)
 305    (hbounded : DeprecatedDefectAnnularCostBounded sensor hm) :
 306    False :=
 307  rh_from_complex_analysis_axioms sensor hm hbounded
 308
 309/-! ### §5. Direct RH from zero-free criterion (analytic route target) -/
 310
 311/-- **Direct RH from a zero-free criterion.**
 312
 313The honest analytic route targets a `ZeroFreeCriterion` (§4 above) which
 314packages bounded log-derivative + carrier nonvanishing + honest phase-family
 315data for witnessed zeros. Once realized, this gives RH without the cost
 316framework contradiction. -/
 317theorem direct_rh_from_zero_free_criterion (zfc : ZeroFreeCriterion) :
 318    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
 319  rh_from_zero_free_criterion zfc
 320
 321/-! ### §6. Canonical frontier inventory -/
 322
 323/-- **Architecture summary (April 2026, inventory frozen):**
 324
 325### Classification of open obligations
 326
 327**ACTIVE** (on critical path to unconditional RH):
 328
 329| Item | Kind | Module | Route |
 330|------|------|--------|-------|
 331| `EulerBoundaryBridgeAssumption` | explicit hypothesis | `UnifiedRH` | Ontology (preferred) |
 332| `HonestPhaseCostBridge` | structure | `AnalyticTrace` | Analytic |
 333| `charge_zero_of_honest_phase` | field in `ZeroFreeCriterion` | `AnalyticTrace` | Analytic |
 334
 335Both active bridges are RH-equivalent:
 336- `EBBA_iff_rh` : `EulerBoundaryBridgeAssumption ↔ (∀ sensor, sensor.charge ≠ 0 → False)`
 337- `HonestPhaseCostBridge_iff_rh` : `HonestPhaseCostBridge ↔ (∀ sensor, sensor.charge = 0)`
 338
 339**ALTERNATE** (valid but not primary):
 340
 341| Item | Kind | Module | Note |
 342|------|------|--------|------|
 343| `VectorCChargeZeroBridge` | structure | `AnalyticTrace` | Requires extra input (`VectorCSymmetryOnlyNoGo`) |
 344| `CompositionClosureHypothesis` | structure | `CompositionDivergence` | Separate conditional certificate |
 345
 346**DEPRECATED** (inconsistent or routed through inconsistent axiom):
 347
 348| Item | Kind | Module |
 349|------|------|--------|
 350| `defect_annular_cost_bounded` | `axiom` | `EulerInstantiation` |
 351| `analytic_rh` | theorem | `AnalyticTrace` |
 352| `rh_chain_summary_legacy` | theorem | `AnalyticTrace` |
 353| `rh_from_single_axiom` | theorem | `ArgumentPrincipleProved` |
 354
 355### Ontology route (preferred, single bridge hypothesis)
 3561. Every sensor has admissible Euler trace. **Proved.**
 3572. Nonzero charge forces cost divergence. **Proved.**
 3583. Collapse-to-proxy transport bridge. **`EulerBoundaryBridgeAssumption` (RH-equivalent).**
 3594. No nonzero-charge sensor exists. **Proved from 1+2+3.**
 360
 361### Pure analytic route
 3621. Euler carrier convergent, nonvanishing, bounded log-derivative. **Proved.**
 3632. Floor coverage ↔ charge = 0. **Proved.**
 3643. Honest witnessed ζ⁻¹ phase data → `ZetaPhaseFamilyData`. **Proved.**
 3654. Honest phase data gives perturbation control and exact zero excess. **Proved.**
 3665. Bounded total cost → charge = 0. **`HonestPhaseCostBridge` (RH-equivalent).** -/
 367theorem rh_frontier_inventory : True := trivial
 368
 369/-- ⚠ DEPRECATED: routes through the inconsistent `defect_annular_cost_bounded`.
 370Use `unified_rh` (ontology) or `direct_rh_from_honestPhaseCostBridge` (analytic). -/
 371theorem rh_chain_summary_legacy :
 372    (∀ (sensor : DefectSensor) (hm : sensor.charge ≠ 0),
 373      DeprecatedDefectAnnularCostBounded sensor hm) →
 374    ∀ (sensor : DefectSensor), sensor.charge ≠ 0 → False :=
 375  fun hbounded sensor hm => analytic_rh sensor hm (hbounded sensor hm)
 376
 377/-! ### §7. Cross-route connection and RH-equivalence
 378
 379The ontology route (`EulerBoundaryBridgeAssumption`) and the analytic route
 380(`HonestPhaseCostBridge`) are both RH-equivalent. The ontology route is
 381strictly stronger: it works for all `DefectSensor`s (abstract), while the
 382analytic route covers `WitnessedDefectSensor`s (actual zeros of ζ).
 383
 384Closing EBBA immediately supplies HonestPhaseCostBridge, ZeroFreeCriterion,
 385and all downstream analytic certificates. -/
 386
 387/-- RH (for witnessed sensors) implies `HonestPhaseCostBridge`. If every
 388witnessed sensor has charge 0, then every honest sampled family has
 389bounded cost because zero-charge families have zero topological floor. -/
 390theorem HonestPhaseCostBridge_of_rh
 391    (hrh : ∀ sensor : WitnessedDefectSensor, sensor.charge = 0) :
 392    HonestPhaseCostBridge where
 393  cost_bounded_of_honest_phase := by
 394    intro sensor zfd hzsensor
 395    have hcharge_sensor : sensor.charge = 0 := hrh sensor
 396    have hcharge_ds : zfd.sensor.charge = 0 := by
 397      simpa [hzsensor] using hcharge_sensor
 398    have hcharge_fam : (zfd.phaseFamily.toSampledFamily).sensor.charge = 0 := by
 399      simpa [DefectPhaseFamily.toSampledFamily, zfd.family_sensor] using hcharge_ds
 400    exact realizedDefectCostBounded_of_charge_zero_and_excessBounded
 401      (zfd.phaseFamily.toSampledFamily) hcharge_fam
 402      (honestPhaseFamily_excess_bounded zfd)
 403
 404/-- `HonestPhaseCostBridge` is logically equivalent to RH (for witnessed
 405sensors).
 406
 407This theorem makes machine-checkable the observation that the bounded-cost
 408bridge is not weaker than RH — it IS RH expressed through the sampled-cost
 409framework. The proof uses `not_realizedDefectAnnularCostBounded` (which
 410shows bounded cost is impossible for nonzero charge) for the forward
 411direction, and zero-charge bounded-cost for the backward direction. -/
 412theorem HonestPhaseCostBridge_iff_rh :
 413    HonestPhaseCostBridge ↔
 414      (∀ sensor : WitnessedDefectSensor, sensor.charge = 0) :=
 415  ⟨fun hb sensor => by
 416    by_contra hm
 417    exact direct_rh_from_honestPhaseCostBridge hb sensor hm,
 418   HonestPhaseCostBridge_of_rh⟩
 419
 420/-! ### §8. Cross-route connection: ontology → analytic -/
 421
 422/-- The ontology bridge immediately supplies the honest-phase cost bridge.
 423This proves closing EBBA closes ALL active routes simultaneously. -/
 424theorem honestPhaseCostBridge_of_EBBA
 425    (bridge : Unification.UnifiedRH.EulerBoundaryBridgeAssumption) :
 426    HonestPhaseCostBridge :=
 427  HonestPhaseCostBridge_of_rh (fun sensor => by
 428    by_contra hm
 429    exact Unification.UnifiedRH.unified_rh bridge sensor.toDefectSensor (by simpa using hm))
 430
 431/-- The ontology bridge also supplies a complete `ZeroFreeCriterion`. -/
 432noncomputable def zeroFreeCriterion_of_EBBA
 433    (bridge : Unification.UnifiedRH.EulerBoundaryBridgeAssumption) :
 434    ZeroFreeCriterion :=
 435  zeroFreeCriterion_of_honestPhaseCostBridge (honestPhaseCostBridge_of_EBBA bridge)
 436
 437/-- Direct witnessed-sensor RH from the ontology bridge through the analytic route. -/
 438theorem direct_rh_from_EBBA_via_analytic
 439    (bridge : Unification.UnifiedRH.EulerBoundaryBridgeAssumption) :
 440    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
 441  rh_from_zero_free_criterion (zeroFreeCriterion_of_EBBA bridge)
 442
 443end AnalyticTrace
 444end NumberTheory
 445end IndisputableMonolith
 446