"""`ged.synth` — automated discriminating VERIFICATION of Yariv §7.3 resonator relations. The method is "book-as-oracle" checking, framed by ANALOGY to program synthesis by sketching (Solar-Lezama; cf. Programming Puzzles arXiv:2102.11137): the book supplies the equations (the "holes"), and this module VERIFIES each against a tri-verification constraint set. To be clear about what it is NOT: there is no synthesizer searching a completion space and no automated counterexample-guided (CEGIS) re-solve loop — the derivations and Lean proofs are hand-written and the verifiers only CHECK supplied, known-correct textbook formulas. Each equation region the OCR segments (``core/yariv_ocr_words.json`` — huridocs Text/Formula boxes) is a hole; the constraint set per hole is the same tri-verification the twin's committed claims carry (``ged.tri_verify``): * a DISCRIMINATING symbolic derivation — sympy SOLVES the physics for the formula, so a wrong prefactor does not follow (the #140 anti-tautology standard). This axis genuinely discriminates for finesse_loss / photon_lifetime / quality_factor; for finesse_linewidth it is definitional (F ≡ FSR/Δν is the DEFINITION of spectral finesse — see that hole); * numeric reproducibility + a finesse cross-validation on a concrete ring; * a real Lean theorem (VVUQ ``lean_verify``, no ``sorry``). NOTE its epistemic weight varies per relation: it proves the formula FOLLOWS FROM its premises, but for the four derived- quantity relations the load-bearing physics is a PREMISE and the proof is an algebraic consolidation — genuine discrimination there rides the sympy axis, not Lean (each hole's Lean ``check`` string says which). The one "counterexample-guided" touch — adding the physical ``0 fail). # Each returns {status, check, detail}; sympy is optional -> honest 'not_run'. # --------------------------------------------------------------------------- _OK = "pass" # Which axis carries the GENUINE discrimination for each relation (peer review, 2026-07-02). # The Lean proves the formula follows from its premises, but for the derived-quantity relations # the load-bearing physics is a PREMISE and the proof is an algebraic consolidation, so the # discrimination rides the sympy axis; finesse_linewidth is definitional (F ≡ FSR/Δν). The full # per-relation rationale is the SSOT in each claim's ``lean.check`` (core/yariv_ch7_resonators.json); # this map is just the short tag the report surfaces (and the tests assert against). _DISCRIMINATION_AXIS: dict[str, str] = { "finesse_linewidth": "definitional", # F ≡ FSR/Δν is the definition of spectral finesse "finesse_loss": "lean+sympy", # a wrong coefficient of finesse fails both axes "photon_lifetime": "sympy", # Lean consolidates the premise Δω=1/τ_p algebraically "quality_factor": "sympy", # Lean consolidates the premises algebraically "q_cross_validation": "sympy", # Lean consolidates the chain algebraically } def _sympy_not_run(check: str) -> dict: return {"status": "not_run", "check": check, "detail": "sympy unavailable — pip install 'ged[triverify]' to run the symbolic layer"} def verify_hole_sympy(slug: str) -> dict: """PURE: the DISCRIMINATING symbolic derivation for a §7.3 hole — sympy solves the physics for the formula (a wrong prefactor does not follow). Mirrors the compiled Lean theorem of the same relation. ``not_run`` when sympy is absent (honest degradation).""" try: import sympy as sp # type: ignore[import-untyped] except ImportError: return _sympy_not_run(f"symbolic derivation for {slug}") if slug == "finesse_linewidth": # DEFINITIONAL consistency check (NOT discriminating against independent physics): the # Airy coefficient is parametrized as (2F/pi)^2 — i.e. by the finesse F ITSELF — so # solving the half-max and forming FSR/FWHM recovers F by construction (it reduces to # F == F). This verifies the DEFINITION F ≡ FSR/Delta_nu is self-consistent with the # Airy half-width FWHM=2pi/F; it does not test F against the ring coupling equations # (that is finesse_loss / finesse_from_transfer). Honest per peer review 2026-07-02. F, delta = sp.symbols("F delta", positive=True) d_half = sp.solve(sp.Eq((2 * F / sp.pi) ** 2 * (delta / 2) ** 2, 1), delta)[0] fwhm_phase = 2 * d_half # full width in round-trip phase f_from_airy = sp.simplify(2 * sp.pi / fwhm_phase) # FSR in phase is 2*pi ok = sp.simplify(f_from_airy - F) == 0 return {"status": _OK if ok else "fail", "check": "DEFINITIONAL: FSR/FWHM with FWHM=2pi/F recovers F (F ≡ FSR/Delta_nu is the definition of finesse)", "detail": "a consistency check of the finesse definition against the Airy half-width — NOT a discriminating derivation (that is on finesse_loss)"} if slug == "finesse_loss": # F = (pi/2)*sqrt(F_c) with the coefficient of finesse F_c = 4*ta/(1-ta)^2. The # coefficient MUST enter the computation (a wrong 4 or a wrong exponent has to fail — # else this is the #140 tautology). Substitute u = 1-ta in (0,1) so sqrt((1-ta)^2) # resolves with the physical sign; build F_c explicitly and take sympy's own sqrt. u = sp.symbols("u", positive=True) # u = 1 - ta, physical: u in (0,1) ta_expr = 1 - u Fc = 4 * ta_expr / u ** 2 # coefficient of finesse (the 4 and the ^2 are load-bearing) f_from_coeff = sp.simplify((sp.pi / 2) * sp.sqrt(Fc)) # sympy takes the root of the ACTUAL F_c f_target = sp.pi * sp.sqrt(ta_expr) / u ok = sp.simplify(f_from_coeff - f_target) == 0 return {"status": _OK if ok else "fail", "check": "(pi/2)*sqrt(F_c) with F_c=4ta/(1-ta)^2 simplifies to pi*sqrt(ta)/(1-ta) on 0 Q = w0*tau. U, tau, w0 = sp.symbols("U tau_p omega_0", positive=True) q_def = 2 * sp.pi * U / ((U / tau) * (2 * sp.pi / w0)) ok = sp.simplify(q_def - w0 * tau) == 0 return {"status": _OK if ok else "fail", "check": "2*pi*(stored)/(lost per period) = omega_0*tau_p", "detail": "Q as the energy-decay ratio reduces to omega_0*tau_p (the stored energy cancels)"} if slug == "q_cross_validation": # Q = w0*tau, tau = 1/(2 pi Delta_nu), Delta_nu = FSR/F, w0 = 2 pi nu0 -> Q = nu0*F/FSR. nu0, F, FSR = sp.symbols("nu_0 F FSR", positive=True) dnu = FSR / F tau = 1 / (2 * sp.pi * dnu) q_chain = (2 * sp.pi * nu0) * tau ok = sp.simplify(q_chain - nu0 * F / FSR) == 0 return {"status": _OK if ok else "fail", "check": "chaining Q=w0*tau_p, tau_p=1/(2pi*FSR/F), w0=2pi*nu0 gives Q = nu0*F/FSR", "detail": "the quality factor closes onto the calibration FSR and the finesse (coordination)"} return {"status": "not_run", "check": f"no symbolic check for {slug}", "detail": ""} # --------------------------------------------------------------------------- # Numeric reproducibility + the cross-validation WEB closure (a concrete ring). # --------------------------------------------------------------------------- @dataclass(frozen=True) class ResonatorPoint: """A concrete operating point the whole §7.3 web is evaluated on: the twin's ring (R, n_g) plus the round-trip amplitude PRODUCT ``ta`` (self-coupling t × round-trip loss a; the resonance sharpness is product-governed) and the probe wavelength.""" radius_m: float n_group: float round_trip_ta: float # the PRODUCT t*a, in (0, 1) — not a single coupler amplitude wavelength_m: float = 1.55e-6 def __post_init__(self) -> None: if not (0.0 < self.round_trip_ta < 1.0): raise ValueError("round_trip_ta (the product t*a) must be in (0, 1)") if self.radius_m <= 0 or self.n_group <= 0 or self.wavelength_m <= 0: raise ValueError("radius, n_group and wavelength must be positive") # The twin's ring (test_yariv_twin: R=49.759 µm, n_g=4.2) at the WC coupling point ta=0.976. YARIV_RING = ResonatorPoint(radius_m=49.759e-6, n_group=4.2, round_trip_ta=0.976) # The finesse cross-validation tolerance. The closed-form finesse F=π√(ta)/(1−ta) is the # high-finesse limit; the transfer-function route MEASURES the finesse numerically from the # ring's own complex response and converges to it as ta→1 (they differ at O((1−ta)²): rel # 2.3e-3 at ta=0.9, 1.2e-4 at ta=0.976, 2e-5 at ta=0.99 — all under 5e-3). 5e-3 is TIGHT # enough that a wrong finesse FORMULA breaks it: a wrong prefactor/exponent diverges by ≫5e-3 # at every ta, and the dropped-√ta error is caught where it matters (1−√ta ≈ (1−ta)/2 relative, # so ~1.2% at ta=0.976 → caught) though it shrinks toward the tol near ta→1 (√ta→1 there, so # that specific error genuinely vanishes — the closure runs at ta=0.976 where it bites). The # transfer route NEVER references the coefficient of finesse F_c, so — unlike the earlier # lineshape route — a wrong SHARED F_c cannot leak into both sides (no common-mode blindness). FINESSE_CONSISTENCY_TOL = 5e-3 def finesse_from_loss(ta: float) -> float: """PURE: the closed-form finesse from the round-trip amplitude (relation finesse_loss), F = pi*sqrt(ta)/(1-ta). This is the high-finesse limit of the exact spectral finesse.""" if not (0.0 < ta < 1.0): raise ValueError("round-trip amplitude ta must be in (0, 1)") return math.pi * math.sqrt(ta) / (1 - ta) def finesse_from_transfer(self_coupling: float, round_trip_amplitude: float, points: int = 4001) -> float: """PURE and GENUINELY INDEPENDENT of the closed-form finesse: MEASURE the finesse from the ring's own complex all-pass through-port response, with the coupler self-coupling ``t`` and the round-trip amplitude ``a`` kept SEPARATE: H(δ) = (t − a·e^{iδ}) / (1 − t·a·e^{iδ}), T(δ) = |H(δ)|² (a resonance NOTCH). Numerically finds the notch's half-depth full width and returns finesse = FSR/FWHM (FSR = 2π in round-trip phase). Crucially the coefficient of finesse F_c = 4ta/(1−ta)² NEVER appears — this route reads the sharpness off the raw transfer function — so a wrong F_c/finesse FORMULA elsewhere cannot leak in (the common-mode-blindness fix the peer review demanded). It agrees with π√(ta)/(1−ta) to ~1e-4 at the twin's operating point (ta=0.976); a wrong closed-form finesse disagrees.""" t, a = self_coupling, round_trip_amplitude if not (0.0 < t < 1.0) or not (0.0 < a < 1.0): raise ValueError("self_coupling and round_trip_amplitude must be in (0, 1)") # ponytail: `notch` duplicates work_contracts.ring_transmission and `_cross` below duplicates # work_contracts._half_crossing (both verified identical). NOT reused here: importing from # work_contracts would be a backwards dependency (synth is a stdlib-only leaf; work_contracts # sits above it, importing arena/sim/solve). The clean fix is to move both physics primitives # DOWN into sim.py (which both modules may sit above) and reuse from there — deferred, as it # touches work_contracts (outside this change) and keeps the F_c-free measurement self-contained. def notch(delta: float) -> float: cos_d, sin_d = math.cos(delta), math.sin(delta) num = (t - a * cos_d) ** 2 + (a * sin_d) ** 2 den = (1 - t * a * cos_d) ** 2 + (t * a * sin_d) ** 2 return num / den # sample a window around the resonance (δ=0) wide enough to contain the notch's half-power # points (window ≈ 24 FWHM). FWHM in phase ≈ 2π/F with F ≈ π√(ta)/(1−ta), i.e. FWHM ≈ # 2(1−ta)/√ta. ta = t*a ∈ (0,1) by the guard above, so no ta≥1 branch is needed. Note the # estimate is only for window sizing; the returned finesse is MEASURED, F_c-free (see above). ta = t * a fwhm_est = 2 * (1 - ta) / math.sqrt(ta) half_window = min(math.pi, 12 * fwhm_est) deltas = [(-half_window) + (2 * half_window) * i / (points - 1) for i in range(points)] transmission = [notch(d) for d in deltas] t_min = min(transmission) t_base = notch(math.pi) # anti-resonance = the notch baseline half = (t_base + t_min) / 2.0 i_min = transmission.index(t_min) left = i_min while left > 0 and transmission[left] < half: left -= 1 right = i_min while right < points - 1 and transmission[right] < half: right += 1 if transmission[left] < half or transmission[right] < half: raise ValueError("notch does not recover to half depth within the window — widen it") def _cross(i0: int, i1: int) -> float: return deltas[i0] + (half - transmission[i0]) * (deltas[i1] - deltas[i0]) / (transmission[i1] - transmission[i0]) f_left = _cross(left, left + 1) f_right = _cross(right - 1, right) return 2 * math.pi / (f_right - f_left) # FSR (=2π in phase) / FWHM @dataclass(frozen=True) class ResonatorMetrics: """The evaluated §7.3 web at a ResonatorPoint. The load-bearing NUMERIC cross-validation is the finesse computed two independent ways — ``finesse_from_loss`` (closed form) vs. ``finesse_from_transfer`` (measured) — see ``finesse_from_transfer`` for why they are genuinely independent. The linewidth, photon lifetime and Q are DERIVED downstream (definitionally from finesse + FSR) and reported, not further-independent checks.""" fsr_hz: float finesse_from_loss: float finesse_from_transfer: float linewidth_hz: float photon_lifetime_s: float quality_factor: float @property def web_closes(self) -> bool: """The load-bearing consistency: the closed-form finesse and the transfer-function- MEASURED finesse agree in the high-finesse regime. A wrong finesse relation diverges.""" return math.isclose(self.finesse_from_loss, self.finesse_from_transfer, rel_tol=FINESSE_CONSISTENCY_TOL) def evaluate_web(point: ResonatorPoint) -> ResonatorMetrics: """PURE: evaluate the §7.3 web on ``point``. The FSR is the calibration (Yariv 7.3-4); the finesse is computed the closed-form way AND measured from the ring's transfer function (the genuinely-independent cross-validation); the linewidth, photon lifetime and Q are derived. The transfer measurement uses the symmetric critical-coupling split t=a=√ta — the resonance sharpness is set by the product ta, so this recovers the same finesse as any (t,a) split.""" fsr = _C_M_PER_S / (2 * math.pi * point.n_group * point.radius_m) # calibration ta = point.round_trip_ta f_loss = finesse_from_loss(ta) # finesse_loss (closed form) sqrt_ta = math.sqrt(ta) # split the product into t=a=√ta f_transfer = finesse_from_transfer(sqrt_ta, sqrt_ta) # measured from |H(δ)|² linewidth = fsr / f_loss # Δν = FSR/F nu0 = _C_M_PER_S / point.wavelength_m photon_lifetime = 1 / (2 * math.pi * linewidth) # photon_lifetime quality_factor = nu0 * f_loss / fsr # q_cross_validation return ResonatorMetrics( fsr_hz=fsr, finesse_from_loss=f_loss, finesse_from_transfer=f_transfer, linewidth_hz=linewidth, photon_lifetime_s=photon_lifetime, quality_factor=quality_factor, ) def verify_hole_numpy(point: ResonatorPoint = YARIV_RING, metrics: "ResonatorMetrics | None" = None) -> dict: """PURE: reproducible-finiteness of the web on a concrete ring AND its cross-validation (the closed-form and transfer-function-measured finesse agree). A non-finite or non-closing web is a 'fail'. ``metrics`` may be a precomputed ``evaluate_web(point)`` to avoid recomputing it.""" m = metrics if metrics is not None else evaluate_web(point) finite = all( isinstance(v, float) and math.isfinite(v) for v in (m.fsr_hz, m.finesse_from_loss, m.finesse_from_transfer, m.linewidth_hz, m.photon_lifetime_s, m.quality_factor) ) ok = finite and m.web_closes return {"status": _OK if ok else "fail", "check": "the §7.3 web evaluates finite and the closed-form finesse matches the transfer-function measurement", "detail": (f"FSR={m.fsr_hz/1e9:.3f} GHz, F_loss={m.finesse_from_loss:.2f}, " f"F_transfer={m.finesse_from_transfer:.2f}, Q={m.quality_factor:.3e} " f"(closure {m.web_closes})") if ok else "web non-finite or the closed-form and measured finesse disagree"} # --------------------------------------------------------------------------- # The synthesis report (assemble the tri-verification per hole; honest anchor axis). # --------------------------------------------------------------------------- def load_lean_results(path: str | None = None) -> dict: """Edge: the packaged real VVUQ lean_verify results, keyed by slug. ``{}`` if absent.""" p = Path(path) if path is not None else _CH7_PATH if not p.exists(): return {} data = json.loads(p.read_text(encoding="utf-8")) return {slug: rec.get("lean", {}) for slug, rec in data.get("claims", {}).items()} def _validation_status(methods: dict) -> str: """PURE: strongest passing axis (lean > sympy > numpy > none). Mirrors tri_verify.""" passed = {m for m, v in methods.items() if (v or {}).get("status") == "pass"} if "lean" in passed: return "verified" if "sympy" in passed: return "verified_symbolic" if "numpy" in passed: return "numeric_only" return "unverified" def synthesize_hole(hole: ResonatorHole, lean_results: dict, point: ResonatorPoint = YARIV_RING, numpy_result: dict | None = None) -> dict: """PURE: fill one hole — run its discriminating sympy derivation + numeric web check, attach the packaged real Lean result, and report the strongest axis. The anchor axis is honestly ``pending`` (math verified; not gated to a printed equation). The numeric web is point-invariant (identical for every hole), so a caller filling all holes can compute it once and pass it in as ``numpy_result`` to avoid recomputing ``evaluate_web`` per hole.""" methods = { "sympy": verify_hole_sympy(hole.slug), "numpy": numpy_result if numpy_result is not None else verify_hole_numpy(point), "lean": lean_results.get(hole.slug) or {"status": "not_run", "check": "no lean result", "detail": ""}, } passed = sorted(m for m, v in methods.items() if (v or {}).get("status") == "pass") return { "slug": hole.slug, "name": hole.name, "normalized_latex": hole.normalized_latex, "normalized_sympy": hole.normalized_sympy, "premises": list(hole.premises), "provenance": hole.provenance, "cross_validates": list(hole.cross_validates), "verification": methods, "verification_method_count": len(passed), "passed_methods": passed, "validation_status": _validation_status(methods), "discrimination_axis": _DISCRIMINATION_AXIS.get(hole.slug, "unspecified"), "anchor_status": "pending", # math axis done; source-anchor (OCR geometry+VLM) is future work } @dataclass class SynthesisReport: """The §7.3 pilot's output: per-hole fills + the web-closure coordination flag.""" section: str holes: list = field(default_factory=list) web_closes: bool = False def to_dict(self) -> dict: return {"section": self.section, "web_closes": self.web_closes, "holes": self.holes} @property def all_math_verified(self) -> bool: """Every hole is math-verified when its strongest axis is a real formal/symbolic proof (not merely a finite number) AND the numeric web closes.""" return self.web_closes and all( h["validation_status"] in ("verified", "verified_symbolic") for h in self.holes ) def synthesize_section(point: ResonatorPoint = YARIV_RING, lean_path: str | None = None) -> SynthesisReport: """PURE (over injected edges): run the §7.3 VERIFICATION over every enumerated relation — check each against the tri-verification constraint set and report the finesse cross- validation. This is book-as-oracle checking (see the module docstring): the relations are the book's equations, the constraints are the verifiers, a relation passes iff all three axes accept and the web stays consistent with the calibration FSR. It is NOT program synthesis — nothing is searched or generated; the derivations and proofs are supplied.""" lean_results = load_lean_results(lean_path) # the numeric web is point-invariant across holes — evaluate it ONCE and reuse. web = evaluate_web(point) numpy_result = verify_hole_numpy(point, web) holes = [synthesize_hole(hole, lean_results, point, numpy_result) for hole in SECTION_7_3_HOLES] return SynthesisReport(section="Yariv §7.3 optical resonators", holes=holes, web_closes=web.web_closes) __all__ = [ "ResonatorHole", "SECTION_7_3_HOLES", "verify_hole_sympy", "ResonatorPoint", "YARIV_RING", "ResonatorMetrics", "evaluate_web", "verify_hole_numpy", "FINESSE_CONSISTENCY_TOL", "finesse_from_loss", "finesse_from_transfer", "load_lean_results", "synthesize_hole", "SynthesisReport", "synthesize_section", ]