CORE25_PROOF_GUIDE.md
Machine Native Reasoning
CORE25_PROOF_GUIDE.md
1 # Core 2.5 — proof guide and correspondence
2
3 ## Source and mathematical types
4
5 The immutable anchor is `source/core_v0.2.tex`, label `r:positive-packets`, original
6 printed page 6 and its setup immediately preceding the statement. The exact source
7 index and bindings are retained. The manuscript treats a real vector space, a
8 convex cone K, a linear mass λ strictly positive on K \ {0}, and a finite complete
9 family of linear packet operators preserving K.
10
11 `ConvexCone ℝ V` supplies actual closure under addition and positive scalar
12 multiplication. Its library definition does not force nonemptiness or zero
13 membership. This is sufficient: a normalized input is separately required to
14 belong to the cone; normalization uses a strictly positive inverse scalar. Thus no
15 extra pointedness, closedness, finite-dimensionality or coordinate positivity is
16 silently added. Strict mass already rules out nonzero zero-mass cone members.
17
18 ## The general mixture
19
20 `StrictMass C mass` is exactly positivity on nonzero cone members.
21 `Preserves C P` checks actual image membership, not a name or intended property.
22 `Complete P` is equality of the finite sum of the supplied operators with the
23 identity. `IsState C mass v` asserts both cone membership and mass one.
24
25 For each index i, `weight mass P v i = mass (P i v)`. Cone preservation and strict
26 mass prove nonnegativity, and zero weight is equivalent to the zero packet.
27 Linearity carries completeness to the sum-of-weights identity. The positive index
28 subtype contains exactly the normalizable packets. Scaling by the inverse weight
29 preserves the cone and gives mass one. Multiplication by the original weight
30 recovers the packet. Finally the omitted terms vanish, so the restricted sum still
31 reconstructs v and its weights still sum to one.
32
33 Principal endpoint: `Komorebi.MachineTheory.PositivePackets.source_core25`.
34 The separate endpoint `sum_positive_weights_one` states the active-weight sum.
35 No idempotence or orthogonality appears in this sector. Positive halves of the
36 identity form a checked complete mixture even though neither half is idempotent.
37
38 ## Coordinate classification
39
40 `Coordinate.cone N` is the actual coordinatewise nonnegative cone on `N → ℝ`.
41 `coefficient P r c` is obtained by applying P to the standard basis vector at c,
42 then evaluating coordinate r. `basis_expansion` and `coordinate_action` establish
43 the link to an arbitrary vector, rather than assuming a matrix representation.
44
45 Preserving the cone is equivalent to every coefficient being nonnegative.
46 Completeness says the coefficient sums are those of the identity. Nonnegative
47 terms summing to zero force all off-diagonal entries to vanish. Hence each map is
48 diagonal. Its idempotence then makes each diagonal coefficient d satisfy d²=d,
49 and the real-field identity implies d=0 or d=1. The diagonal sum being one gives
50 exactly one owner for every coordinate. The constructed owner map represents the
51 original operators as coordinate selectors. Different owners have disjoint ranges
52 and their cross compositions are zero.
53
54 `source_core25_coordinate` returns that concrete representation, unique ownership
55 and disjoint composition. `classification_iff` also proves every such selector
56 family is positive, complete and idempotent. Thus the result is a characterization,
57 not only a necessary condition. No positive coordinate dimension, nonempty index
58 type, pairwise-orthogonal assumption, or surjective ownership assumption is added.
59 An index may own no coordinates and represent the zero operator.
60
61 ## Coordinate changes
62
63 For a linear equivalence e, `Transport` pushes the cone forward, pulls the mass
64 back by e⁻¹, and conjugates the packet maps. It proves preserved state membership,
65 strict mass, completeness, idempotence where supplied, equality of weights, and
66 equality of normalized packets after applying e. `source_coordinate_change`
67 collects the hypotheses needed to apply the general mixture theorem in the new
68 coordinates. It is not a theorem that signed coordinates are valid in the old
69 coordinate cone with the old mass left unchanged.
70
71 A real shear sends a normalized nonnegative state to (-1,1). It belongs to the
72 transported cone and has unit transported mass, despite its negative first
73 coordinate. The Haar detail example is different: it remains outside the declared
74 positive cone and has zero mass without vanishing. Coordinate signs alone cannot
75 replace the cone and mass contract.
76
77 ## Source-facing checks and boundaries
78
79 `checks/CheckPositivePacketsAPI.lean` checks the source theorem from raw linear
80 maps, pointwise membership hypotheses, actual operator-sum equality and normalized
81 input. It independently checks the coordinate result from raw nonnegative inputs,
82 without assuming the bundled definitions as conclusions.
83
84 Eleven negative fixtures test omitted strict mass, omitted cone preservation,
85 omitted completeness, nonunit input, zero-packet normalization, non-idempotent
86 positive halves, overlapping projectors, incorrect coordinate-sign inference and
87 an unchanged mass after coordinate transport. They must fail for the expected
88 proof diagnostics, not name-resolution errors, missing imports or timeouts.
89
90 These declarations establish mathematical constructions. Some use classical choice
91 and are noncomputable. They do not certify a learned representation, numerical
92 stability, a physical probability model, or the Python checker in all executions.
93 The standard axioms and recorded Lean/dependency environment remain trusted.