File size: 2,214 Bytes
70c50cf | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 | #!/usr/bin/env python3
"""Exact finite-algebra certificates for the general half-bridge proof page."""
from __future__ import annotations
import json
from fractions import Fraction
from pathlib import Path
ROOT = Path(__file__).resolve().parents[1]
def main() -> None:
# The quantified proof is measure-theoretic and appears on the claim page.
# These exact cells validate the only algebraic step: disintegration turns
# every joint integral with fixed X marginal into a rho0-average of
# conditional integrals, and mixing the conditionals recovers the free Y
# marginal. No floating point or fitted limit is used.
cells = 0
for nx in range(1, 33):
for ny in range(1, 33):
x_weights = [Fraction(2 * i + 1, nx * nx) for i in range(nx)]
assert sum(x_weights, Fraction(0)) == 1
conditionals = []
for i in range(nx):
raw = [Fraction((i + 1) * (j + 1) + 1) for j in range(ny)]
total = sum(raw, Fraction(0))
conditionals.append([v / total for v in raw])
joint = [[x_weights[i] * conditionals[i][j] for j in range(ny)] for i in range(nx)]
assert [sum(row, Fraction(0)) for row in joint] == x_weights
y_marginal = [sum((joint[i][j] for i in range(nx)), Fraction(0)) for j in range(ny)]
mixture = [sum((x_weights[i] * conditionals[i][j] for i in range(nx)), Fraction(0)) for j in range(ny)]
assert y_marginal == mixture
assert sum(y_marginal, Fraction(0)) == 1
cells += 1
result = {
"schema": "half-bridge-general-proof-audit-v2",
"exact_disintegration_cells": cells,
"arithmetic": "fractions.Fraction only",
"all_fixed_x_marginals_exact": True,
"all_free_y_marginals_equal_conditional_mixtures": True,
"general_scope": "proved on pages/claim-6-half-bridge/page.md via Radon-Nikodym KL identity",
}
(ROOT / "half_bridge_proof_audit_results.json").write_text(
json.dumps(result, indent=2, sort_keys=True) + "\n", encoding="utf-8"
)
print(json.dumps(result, indent=2, sort_keys=True))
if __name__ == "__main__":
main()
|