CORE25_CORRESPONDENCE_AUDIT.md
Machine Native Reasoning
CORE25_CORRESPONDENCE_AUDIT.md
1 # Core 2.5 source/statement review
2
3 This is an additional source-and-proof inspection in the same assistant session,
4 not an independent external referee or separate proof kernel.
5
6 | Source clause | Actual formal route | Boundary retained |
7 |---|---|---|
8 | Real vector space and convex cone | `ConvexCone ℝ V`, actual cone membership | No ambient dimension or closedness added |
9 | Strict positivity of mass | `StrictMass` and `mass_zero_iff` | Not mere nonnegativity |
10 | Finite complete maps | `Fintype I`, `Complete` | No countably infinite sums |
11 | Nonnegative weights and total one | `weight_nonneg`, `sum_weights_one` | Input has mass one |
12 | Positive normalized components | `PositiveIndex`, `normalized_isState` | No inverse-zero normalized state |
13 | Zero weights vanish | `weight_zero_iff` | Requires actual cone preservation |
14 | Exact mixture reconstruction | `mixture_reconstruction` | Every omitted term is proved zero |
15 | Standard-cone idempotents | `Coordinate.classification_iff` | Coordinate cone and idempotence explicit |
16 | Disjoint coordinate selection | `source_core25_coordinate` | Derived, not assumed |
17 | Coordinate dependence of signs | `Transport`, real shear example | Cone and mass change together |
18
19 The source propositions and proof text remain byte-identical. The formalization
20 has separate endpoints for the two source sectors. The raw API checks their joint
21 coverage. The theorem map also includes covariance as supporting material, not an
22 additional source-result count. The empty-coordinate example and empty-index
23 normalization impossibility prevent accidental strengthening by positivity of
24 cardinality. No claim of full-book formalization follows from this one admission.