COS Method: formal continuation

Download original file

This is the original source text. Reading it does not run or verify the program.

1 {
2   "checkpoint": "0.1.0",
3   "verification_authority": "verification/accepted/run.json",
4   "entries": [
5     {
6       "obligation": "finite_gram_algebra",
7       "status": "EXISTING",
8       "module": "FiniteGram.lean",
9       "scope": "Exact real finite sums; not floating execution."
10     },
11     {
12       "obligation": "enclosure_arithmetic",
13       "status": "EXISTING",
14       "module": "Certificates.lean",
15       "scope": "Consequences of valid supplied enclosures."
16     },
17     {
18       "obligation": "measurable_probability_interface",
19       "status": "CHECKED_IN_SCOPE",
20       "module": "TailProbability.lean",
21       "scope": "Actual measures and measurable final statistics."
22     },
23     {
24       "obligation": "concrete_independent_gaussian_coordinates",
25       "status": "CHECKED_IN_SCOPE",
26       "module": "GaussianTail.lean",
27       "scope": "Actual finite product measure; not a distribution hypothesis."
28     },
29     {
30       "obligation": "symmetric_standard_gaussian_reduction",
31       "status": "CHECKED_IN_SCOPE",
32       "module": "SpectralGaussian.lean",
33       "scope": "Spectral theorem and Gaussian basis invariance; retains zero eigenvalues."
34     },
35     {
36       "obligation": "central_linear_gaussian_image",
37       "status": "CHECKED_IN_SCOPE",
38       "module": "CentralLinearImage.lean",
39       "scope": "X=BZ, singular B allowed; not noncentral or covariance byte decoding."
40     },
41     {
42       "obligation": "finite_matrix_to_spectral_law",
43       "status": "CHECKED_IN_SCOPE",
44       "module": "MatrixGaussian.lean",
45       "scope": "Original Gram definitions to exact mathematical eigenvalues."
46     },
47     {
48       "obligation": "rational_acceptance",
49       "status": "CHECKED_IN_SCOPE",
50       "module": "Acceptance.lean",
51       "scope": "Exact rational Boolean and conditional real soundness; Python integration remains."
52     },
53     {
54       "obligation": "numerical_eigenvalue_inclusion",
55       "status": "OPEN",
56       "module": null,
57       "scope": "Approximate eigensystem and rounding/residual bounds not constructed here."
58     },
59     {
60       "obligation": "exponential_tilting",
61       "status": "OPEN",
62       "module": null,
63       "scope": "Next block: actual density, normalization, integral identity."
64     },
65     {
66       "obligation": "COS_and_packet_remainders",
67       "status": "OPEN",
68       "module": null,
69       "scope": "Support/alias, packet, and omitted-mode bounds."
70     },
71     {
72       "obligation": "directed_arithmetic_and_transcendentals",
73       "status": "OPEN",
74       "module": null,
75       "scope": "Exact semantics and all implementation obligations."
76     },
77     {
78       "obligation": "input_and_output_encoding",
79       "status": "OPEN",
80       "module": null,
81       "scope": "Binary64/decimal parsing and outward serialization."
82     },
83     {
84       "obligation": "covariance_and_noncentral_extensions",
85       "status": "OPEN",
86       "module": null,
87       "scope": "Interpret covariance inputs and prove noncentral shift separately."
88     },
89     {
90       "obligation": "complete_executable_end_to_end",
91       "status": "OPEN",
92       "module": null,
93       "scope": "The composition theorem still has spectral and endpoint certificate premises."
94     }
95   ],
96   "verification_status": "PASS"
97 }

Back to source controls

Back to COS Method: formal continuation