FORMAL_STATUS.md
ABC: source and evidence reader
FORMAL_STATUS.md
1 # ABC formal evidence
2
3 **Final report, 8 October 2026.** KTG passed its exact-version replay. The
4 original ABCJet module built with two retained style warnings. Its explicitly
5 patched copy passed direct elaboration with warnings treated as errors.
6
7 ## Normalized claim and verdict
8
9 The KTG claim is a typed, conditional theorem: for abstract data `D`, certificate
10 semantics `S`, normalization data `N`, a supplied `SourceWitnessTheorem D S N`,
11 a certified realization, a normalization witness, and a monotone observable,
12 the q-pilot observable is bounded by the observable of the output hull.
13 The formal implication is proved as written. An application to the actual IUT
14 objects is incomplete. The smallest unsupplied theorem is
15 `KTG.IUT312.StepXiEWitnessPreservation` for an actual IUT instantiation.
16
17 This is a source-shaped abstract interface. Its named fields and source map do
18 not themselves authenticate their interpretation as the objects and theorems
19 of IUT. The finite Boolean countermodel establishes independence inside this
20 interface. It is not a counterexample to IUT III Corollary 3.12 or to ABC.
21
22 ## Recovered inputs and distinct histories
23
24 | Input | Source pin | Historical status | Fresh status |
25 |---|---|---|---|
26 | Original ABC Jet Determinant Block 01 | Lean and mathlib v4.19.0 | Seven elementary scripts were not compiled in their authoring runtime | Build and seven axiom checks passed, with two style warnings. The stricter warning-as-error source check failed on those warnings |
27 | ABCJet checked copy in this edition | The same Lean and mathlib pins | Two disclosed tactic-sequencing edits to a separate copy | Build, direct warning-as-error elaboration and seven axiom checks passed |
28 | KTG Block 03 v0.3.0 | Lean 4.34.0-rc2, commit `6a10ac8c22beadecabdbb0919c2b50214762f91d` | Checked release dated 17 September 2026 | Clean build and 22 warning-as-error direct elaborations passed |
29
30 The original KTG ZIP has SHA-256
31 `aab95b7b4bdf5e80908aa75917ea37a7ec2a1d8b66eec9faa09704d9e989a94b`.
32 Its ZIP CRC check and all 131 entries of its SHA-256 and size manifest passed.
33 The recovered fresh-replay JSON is historical evidence, rather than the
34 current run. Current input checks are in `formal/INPUT_AUTHENTICATION.json`.
35
36 The ABCJet ZIP has SHA-256
37 `8fa40fc2c39b13ed0eb05fde23a0a08d1e3426b189d0b7ec29b91f51d658bf8c`.
38 Its CRC check passed. The original module SHA-256 is
39 `6e7d9ca58b6b4591696c5afb55f13aec71cd6225bae6b2734acdfd05919b9fb5`.
40 The original module, project file and toolchain file are preserved unchanged
41 in `formal/jet_source`. Their hashes are in
42 `formal/ABCJet_INPUT_AUTHENTICATION.json`.
43
44 ## Current KTG checks
45
46 The unchanged recovered verifier `verification/verify_block03.py --clean`
47 completed with exit code zero. It used the exact declared compiler and Lake
48 5.0.0-src+6a10ac8. The clean build completed all 24 Lake jobs. All 22 Lean source
49 files elaborated directly with warnings treated as errors. The placeholder and
50 custom axiom declaration scan had no hits. The 14 predecessor module files
51 matched their recorded source hashes. Source bytes before and after the run
52 matched.
53
54 The original contract audit is a text-marker check. Its
55 `iut_specific_global_instance_present` field is recorded as a literal `false`
56 by the verifier, rather than computed by an instantiation search. That flag
57 alone is not proof of absence. The raw-source review and the recorded
58 `SourceWitnessTheorem` references locate the supplied inhabitant only in the
59 finite `SourceExample` namespace. The declarations and inspection limit are
60 recorded in `formal/KTG_SOURCE_BOUNDARY_INSPECTION.json`.
61
62 A fresh `#print axioms` audit covered all 42 explicit named KTG theorems. Of
63 these, 41 depend on no axioms. The generic theorem
64 `KTG.Countermodels.prewitness_gates_do_not_imply_hull_witness` uses Lean's
65 standard `propext`. There is no custom axiom or `sorryAx` in the output.
66 The source-specific Boolean countermodel and positive equality model use no
67 axioms. The target list and actual output are preserved in
68 `formal/KTG_AXIOM_TARGETS.json` and `formal/ktg_axiom_audit.log`.
69
70 ## Environment correction and failures
71
72 Both exact official compiler releases were downloaded. The v4.34.0-rc2 archive
73 matched the SHA-256 supplied by the official GitHub API. The v4.19.0 release API
74 did not supply a digest. Its HTTPS source, size and freshly computed digest are
75 recorded without claiming a second independent digest check.
76
77 The first tar extraction commands failed with exit code 2 because this host
78 rejected the packaged numeric ownership. Re-extraction with `--no-same-owner`
79 passed. The official Lean binaries then failed before compilation because the
80 host denies `/proc/<calling-process-PID>/exe`, while allowing `/proc/self/exe`.
81 The official Lean runtime source identifies that lookup. A small `LD_PRELOAD`
82 compatibility shim redirects only this own-process executable lookup to
83 `/proc/self/exe`. Every other path is passed unchanged. The shim is disclosed,
84 hashed and included as source. Compiler and proof bytes were unchanged.
85
86 The direct compiler version checks, clean build, all per-file elaborations and
87 axiom audit passed with that shim. Their reports explicitly record its use.
88 This is a current exact-version replay with a host compatibility layer, rather
89 than a claim that the unassisted executables ran in this host.
90
91 `formal/RUNTIME_FAILURES.md`, the version diagnostics, API metadata, extraction
92 logs and command records retain the failed and corrected attempts. An attempted
93 `strace` diagnosis was denied by the host's ptrace restriction and is also
94 preserved. No infrastructure failure is interpreted as a failed theorem.
95
96 ## Dependency graph and open boundary
97
98 1. `TypedData` gives separate type fields for output, q-pilot, hull-input,
99 comparable-line, prime-strip, trace, arithmetic-structure and measurement roles.
100 2. `SourceRealizationCertificate` contains IPL, an APT trace carrying SHE, and
101 an obstruction bundle. It contains no hull-containment or scalar-bound field.
102 3. `ObstructionControl` demands separate proof predicates for nine channels.
103 4. `NormalizationWitness` contains a comparable-line object and proofs for
104 determinant and procession compatibility. Its tracked grade equation follows.
105 5. **Open application input:** a proof of `StepXiEWitnessPreservation` for
106 actual IUT data yields `QPilotHullContainment`.
107 6. A monotone observable converts that containment into the scalar inequality.
108
109 The separate type fields distinguish roles in the generic interface. They do
110 not require pairwise unequal types. The finite models assign `Bool` to several
111 roles. The normalization grade's `vectorRank` field is only a positive natural
112 number. The comment describing a rank greater than one is not an encoded
113 rank-greater-than-one hypothesis. The grade-transfer equations and the later
114 `j * j` field are checks of the chosen abstract definitions. They do not prove
115 that those definitions match IUT's actual normalization or log-volume objects.
116 Those interpretation and instantiation obligations remain external to the
117 compiler check.
118
119 | Obligation | Audit status | Evidence or boundary |
120 |---|---|---|
121 | Abstract types and theorem quantifiers | Passed | Exact sources and direct elaboration |
122 | Typed certificate has no scalar target field | Passed | `IUT312Certificates.lean` |
123 | Explicit intermediate line and grade bridge | Passed | `IUT312Normalization.lean` |
124 | Conditional hull-to-scalar implication | Passed | `IUT312WitnessObligation.lean` and axiom output |
125 | Pre-witness fields logically imply containment | Refuted in the abstract interface | Boolean equality-order model with output false and q-pilot true |
126 | Actual IUT instantiation of field semantics | Not addressed by compilation | Source interpretation and mathematical instantiation remain separate |
127 | Actual IUT source witness theorem | Open | No inhabitant supplied outside the finite equality example |
128 | IUT III Corollary 3.12 or ABC from this development | Incomplete | The application-specific containment theorem is missing |
129
130 ## ABCJet theorem scope
131
132 The separate ABCJet source contains exactly the following seven statements.
133 Its original broad `import Mathlib` and all seven proof bodies are unchanged
134 during recovery. The resolved mathlib tag is commit
135 `c44e0c8ee63ca166450922a373c7409c5d26b00b`. The nine resolved package commits
136 are retained in `formal/ABCJet_DEPENDENCY_PINS.json`.
137
138 | Theorem | Quantified arithmetic domain and hypotheses | Exact scope |
139 |---|---|---|
140 | `balanced_ratio` | Rational `a,b,c,R`, with `a,b,R` nonzero | Cancellation of the balanced `a*b` factor |
141 | `two_node_gram` | Four arbitrary rational weights and nodes | A two-node polynomial Gram identity |
142 | `three_node_gram` | Six arbitrary rational weights and nodes | A three-node polynomial Gram identity |
143 | `truncatedH2_formula` | Arbitrary rational `t` | Formula for the explicitly defined three-term truncation |
144 | `cleared_truncation` | Rational `a,c`, with `c` nonzero | Denominator-cleared formula for that truncation |
145 | `cleared_truncation_remainder` | Arbitrary integers `a,c` | Exact polynomial decomposition with remainder `a^5` |
146 | `determinant_in_jet_coordinates` | Three arbitrary rational symbols | An algebraic change of coordinates |
147
148 The Gram identities do not encode positivity or nonvanishing hypotheses.
149 The three-term truncation is not the infinite polylogarithm series. The
150 integer remainder identity does not itself formalize a prime-divisibility
151 argument. The final coordinate identity treats three rational symbols and
152 does not establish their equality to analytic or p-adic values. Infinite
153 convergence, general Hankel determinants, valuation-minimality and the
154 global ABC bridge are outside these seven scripts.
155
156 ## Current ABCJet checks and the explicit corrected copy
157
158 The original `lake build` completed successfully under Lean 4.19.0, commit
159 `6caaee842e94`, and Lake 5.0.0-6caaee8. All seven original proofs compiled.
160 The compiler reported two `linter.unnecessarySeqFocus` style warnings at
161 lines 19 and 53. A direct run with `-DwarningAsError=true` rejected those
162 warnings. This unsuccessful strict run is retained as a valid unsuccessful
163 provenance record, rather than reported as a pass or a mathematical failure.
164
165 The original compiled module passed its seven `#print axioms` checks. Six
166 theorems depend on the standard Lean axioms `propext`, `Classical.choice` and
167 `Quot.sound`. The integer remainder identity depends only on `propext`.
168 No `sorryAx` or custom axiom dependency appeared.
169
170 A separate copy in `formal/jet_checked_source` makes exactly the compiler's
171 two suggested changes: `field_simp [ha, hb, hR] <;> ring` becomes
172 `field_simp [ha, hb, hR]; ring`, and `field_simp [hc] <;> ring` becomes
173 `field_simp [hc]; ring`. The original source is untouched. The theorem
174 statements, coefficient domains, constants and broad `import Mathlib` are
175 unchanged. The patch, locations and hashes are in
176 `formal/ABCJet_CHECKED_COPY_PATCH.diff` and its JSON record.
177
178 That checked copy passed its build, direct source elaboration with warnings
179 treated as errors, forbidden-token scan and seven axiom reports. Its source
180 bytes before and after the run matched. No linter was disabled.
181
182 ## Run provenance and reproduction
183
184 The KTG replay, original ABCJet strict failure, and ABCJet checked-copy pass
185 each have a version 2 computation-audit manifest. All three manifests passed
186 the current validator with the project root supplied, including output hashes
187 and execution-input freshness. Validation authenticates the run record, rather
188 than the mathematical source interpretation. Actual validation commands,
189 stdout, exit status and manifest hashes are in
190 `formal/MANIFEST_VALIDATION.json`.
191
192 The exact command records, actual runtime versions, source hashes, shim hash,
193 logs, per-file checks and declared results are preserved. The compilation
194 contracts quantify over the 22 KTG source files and seven ABCJet statements.
195 They are not searches over ABC triples. The Lean proofs quantify over their
196 stated abstract, rational or integer objects, while their application to
197 unencoded analytic and arithmetic objects remains outside the formal scope.
198
199 The strongest safe statement is that the abstract KTG pipeline, its positive
200 model and its logical independence model have been replayed under the exact
201 recorded compiler, and the seven elementary ABCJet identities have been
202 compiler checked under their original exact compiler and mathlib pins. The
203 next mathematical check is a concrete source
204 instantiation of one load-bearing witness-preservation implication. Another
205 generic scalar lemma cannot supply that input.