PROOF_MAP.json
Large Signal Model
PROOF_MAP.json
This is the original source text. Reading it does not run or verify the program.
1 {
2 "purpose": "Navigation from the theoretical atlas into the unchanged accepted formal source",
3 "fresh_Lean_execution": false,
4 "plates": [
5 {
6 "plate": 1,
7 "propositions": [
8 {
9 "id": 1,
10 "title": "Exact realization and consistency",
11 "scope": "Algebraic realization works on arbitrary types. Norm estimates use continuous linear maps on normed spaces. The divided lower bound explicitly assumes the observation space is nontrivial, so the synthesis norm is positive. No orthogonality is inferred.",
12 "modules": [
13 "KomorebiLSM/Normed.lean",
14 "KomorebiLSM/Realization.lean"
15 ]
16 }
17 ]
18 },
19 {
20 "plate": 2,
21 "propositions": [
22 {
23 "id": 2,
24 "title": "Coherent transport and operator realization",
25 "scope": "Total operations on consistent coefficient subtypes. A reference chart is explicitly supplied, making the family nonempty. Partial-map admissible-domain extensions mentioned in surrounding prose are not covered.",
26 "modules": [
27 "KomorebiLSM/Realization.lean"
28 ]
29 }
30 ]
31 },
32 {
33 "plate": 3,
34 "propositions": [
35 {
36 "id": 6,
37 "title": "Exact quotient criterion",
38 "scope": "Reduced-map existence is constructed from fiber constancy, not assumed. Uniqueness is on the actual image, and action-indexed closure is included.",
39 "modules": [
40 "KomorebiLSM/PredictiveClosure.lean"
41 ]
42 },
43 {
44 "id": 7,
45 "title": "Closure defect and compositional defect",
46 "scope": "Actual linear maps and continuous-linear-map operator norm. Idempotence is explicit, and orthogonality is not needed for the algebraic identity. Closure is not assumed in order to prove its criterion.",
47 "modules": [
48 "KomorebiLSM/LinearClosure.lean",
49 "KomorebiLSM/Normed.lean"
50 ]
51 }
52 ]
53 },
54 {
55 "plate": 4,
56 "propositions": [
57 {
58 "id": 8,
59 "title": "Minimal linear predictive completion",
60 "scope": "Known linear dynamics on a finite-dimensional vector space over a field. Iteration adds actual dual-map images of observable row subspaces. Stabilization is proved by strict dimension growth within dim(X)-dim(W0), with persistence after equality and least common invariant extension. Evaluation and arbitrary-basis state maps, linearly independent rows, linear readout H and action transitions B are constructed. Any competing linear summary retaining the initial output and closing under the dynamics contains this completed row space. The subspace/basis construction is noncomputable Lean mathematics, not an implemented numerical row-reduction learner or a proof that new observables are measurable from the original data. The surrounding single-operator Cayley-Hamilton discussion is not an additional coverage claim.",
61 "modules": [
62 "KomorebiLSM/InvariantCompletion.lean",
63 "KomorebiLSM/PredictiveCompletion.lean"
64 ]
65 },
66 {
67 "id": 14,
68 "title": "Exact causal delay closure",
69 "scope": "Positive delay length. Actual observation maps, not empirical ranks. Kernel factorization, range-valued transition, uniqueness, rank-nullity equivalence, dimension-bound stabilization and warm-up-indexed future output are derived over finite-dimensional field vector spaces. The zero-dimensional case does not license a last block for h=0.",
70 "modules": [
71 "KomorebiLSM/DelayClosure.lean"
72 ]
73 }
74 ]
75 },
76 {
77 "plate": 5,
78 "propositions": [
79 {
80 "id": 3,
81 "title": "Complete refinement preserves reconstruction",
82 "scope": "Finite rooted structural trees with nonempty finite child families, arbitrary mixed-depth selections, and the actual condition of exactly one selected node on each full root-to-leaf path. Local parent=sum(children) gives global operator/signal reconstruction. Local sibling-range orthogonality gives the squared-norm identity over real or complex inner-product spaces. A self-adjoint zero-product lemma supplies that orthogonality from projector assumptions. Antichain completeness and energy conservation are conclusions, not assumed aggregate equations. No general best-basis optimization is included.",
83 "modules": [
84 "KomorebiLSM/PacketTree.lean",
85 "KomorebiLSM/TreeEnergy.lean"
86 ]
87 },
88 {
89 "id": 4,
90 "title": "Transfer reconstruction and refinement",
91 "scope": "Actual linear maps between possibly different spaces, with explicit finite completeness and intermediate idempotence. The algebra works under weaker assumptions than orthogonality.",
92 "modules": [
93 "KomorebiLSM/Transfer.lean"
94 ]
95 },
96 {
97 "id": 5,
98 "title": "Polynomial packet interactions",
99 "scope": "All ordered multilinear interactions, including repeated packet indices. The finite polynomial sum retains every cross term. No general nonlinear dictionary discovery is claimed.",
100 "modules": [
101 "KomorebiLSM/Polynomial.lean"
102 ]
103 },
104 {
105 "id": 20,
106 "title": "Packet-interaction truncation bound",
107 "scope": "Continuous multilinear maps retain ordered interaction tuples and their multiplicities. Restricted product-of-packet-range norm bounds yield the exact omitted sum and its amplitude majorant. Telescoping yields the retained Lipschitz bound on the declared ball. Contractivity is explicitly derived for actual orthogonal subspace projectors. The finite-dimensional real Hilbert sector is included in a stronger normed-space algebraic theorem. A separate bound is required for an unexpanded nonpolynomial law and for keeping trajectories inside the domain.",
108 "modules": [
109 "KomorebiLSM/PacketApproximation.lean",
110 "KomorebiLSM/ReconciliationHilbert.lean"
111 ]
112 }
113 ]
114 },
115 {
116 "plate": 6,
117 "propositions": [
118 {
119 "id": 7,
120 "title": "Closure defect and compositional defect",
121 "scope": "Actual linear maps and continuous-linear-map operator norm. Idempotence is explicit, and orthogonality is not needed for the algebraic identity. Closure is not assumed in order to prove its criterion.",
122 "modules": [
123 "KomorebiLSM/LinearClosure.lean",
124 "KomorebiLSM/Normed.lean"
125 ]
126 }
127 ]
128 },
129 {
130 "plate": 7,
131 "propositions": [
132 {
133 "id": 10,
134 "title": "Exact projected memory and a conditional tail bound",
135 "scope": "Exact recurrence elimination, lag reindexing, actual projected blocks, continuous-map bridge, same-history geometric truncation bound and initial-term bound. Nonnegative radius/rho and rho<1 are explicit for the bound. H<=t for full-minus-truncated history; the omitted Ico tail also handles an empty interval. No recursively predicted rollout stability is inferred.",
136 "modules": [
137 "KomorebiLSM/Memory.lean",
138 "KomorebiLSM/MemoryBounds.lean"
139 ]
140 },
141 {
142 "id": 19,
143 "title": "Uniform prediction bound for a stable finite-memory truncation",
144 "scope": "The predictor uses its own recursively generated history, with integer time indices and an explicit initialization window. A strict norm-sum gain below one yields the actual supremum error bound. Coefficient, geometric memory-tail and initialization-forcing budgets are derived and inserted into the recursive theorem. Zero prehistory handles H=0 and t<H without natural-number subtraction artifacts. Retaining the exact forcing removes its contribution. The condition is sufficient, not necessary; failure of this certificate is not proof of instability.",
145 "modules": [
146 "KomorebiLSM/MemoryApproximation.lean",
147 "KomorebiLSM/MemoryStability.lean"
148 ]
149 }
150 ]
151 },
152 {
153 "plate": 8,
154 "propositions": [
155 {
156 "id": 18,
157 "title": "Compositional defect propagation",
158 "scope": "The theorem permits genuinely time-indexed normed state spaces and representations. It defines local residuals from the true transition and approximate step, derives the one-step error, and proves the manuscript suffix-product/sum bound. Lipschitz constants are nonnegative; both true and predicted inputs must lie in the declared domain. Output decoding, constant contraction and exact closure-versus-fit decomposition are separate theorems. An arbitrary changed policy is not automatically covered.",
159 "modules": [
160 "KomorebiLSM/DefectPropagation.lean"
161 ]
162 }
163 ]
164 },
165 {
166 "plate": 9,
167 "propositions": [
168 {
169 "id": 14,
170 "title": "Exact causal delay closure",
171 "scope": "Positive delay length. Actual observation maps, not empirical ranks. Kernel factorization, range-valued transition, uniqueness, rank-nullity equivalence, dimension-bound stabilization and warm-up-indexed future output are derived over finite-dimensional field vector spaces. The zero-dimensional case does not license a last block for h=0.",
172 "modules": [
173 "KomorebiLSM/DelayClosure.lean"
174 ]
175 },
176 {
177 "id": 15,
178 "title": "Data-span identification and its boundary",
179 "scope": "Actual sample and successor linear maps. Kernel compatibility is equivalent to ambient extension, all fits agree on the sampled span, and span invariance is equivalent to successor-image inclusion. The orthogonal Moore-Penrose inverse is constructed using quotient factorization and orthogonal projections, with all four Penrose conditions proved. A proper subspace admits distinct extensions. Classical choices support a symbolic real operator, not an executable floating-point algorithm.",
180 "modules": [
181 "KomorebiLSM/DataSpan.lean",
182 "KomorebiLSM/Pseudoinverse.lean"
183 ]
184 },
185 {
186 "id": 16,
187 "title": "Fixed-space identification bound",
188 "scope": "Finite-dimensional real Hilbert spaces, with the spectral operator norm. The smallest row singular value is represented by the infimum of adjoint norm ratios, proved equal to the infimum on unit vectors. Strict input error below this value derives surjectivity and the norm of the constructed orthogonal pseudoinverse. The full residual identity and divided bound are derived. Coordinates and dimension are fixed. No fitted-basis or statistical error is absorbed without a bound.",
189 "modules": [
190 "KomorebiLSM/IdentificationBound.lean"
191 ]
192 },
193 {
194 "id": 17,
195 "title": "Finite-prefix indistinguishability",
196 "scope": "For every natural horizon T, two explicit rational systems on Fin (T+2) have identical outputs at all times through T and different output at T+1. Their transition powers at T+2 vanish. No bound on the unknown hidden dimension is assumed.",
197 "modules": [
198 "KomorebiLSM/FinitePrefix.lean"
199 ]
200 }
201 ]
202 },
203 {
204 "plate": 10,
205 "propositions": [
206 {
207 "id": 27,
208 "title": "Minimal finite behavior realization",
209 "scope": "The behavior space is the actual real linear span of history/test columns on finite chronological words. Branch operators are constructed by restriction of test shifts, rather than postulated well-defined coordinate maps. Rank means finite dimension of this full column space, not a sampled matrix rank. Every finite linear realization has at least that dimension. Reachable and observable realizations are explicitly isomorphic, intertwining the initial vector, all operators and mass; the intertwiner is unique. Conditional predictions use the true word/history ratio on positive histories. Nonnegativity and causal normalization are separate supplied word-law assumptions. Infinite-record probability measures and the auxiliary supremum-of-finite-submatrix characterization are not additional claims of this mapping. No model is learned from a finite noisy sample here.",
210 "modules": [
211 "KomorebiLSM/BehaviorMinimality.lean",
212 "KomorebiLSM/BehaviorProbability.lean",
213 "KomorebiLSM/BehaviorSpace.lean"
214 ]
215 },
216 {
217 "id": 28,
218 "title": "Observable table reconstruction",
219 "scope": "Finite core coordinates are actual selected test evaluations. An invertible square population matrix gives surjectivity and a lower rank bound; an explicit global finite behavior-rank upper bound supplies injectivity and full coverage. The formula G_s H^{-1} is an actual matrix expression using the correct inverse side. It yields the full chronological state, mass and probability for every word, a reachable observable model and minimal dimension against every finite linear realization. A distinguished selected empty test is the literal mass coordinate (index zero in Fin r). Normalized updates require positive evidence for probabilistic interpretation. Finding the core, deriving an unknown global rank bound and statistical estimation of table entries are not claimed. Noncomputable inverse/space constructions do not amount to an executed numerical data learner.",
220 "modules": [
221 "KomorebiLSM/ObservableCore.lean",
222 "KomorebiLSM/ObservableRealization.lean"
223 ]
224 }
225 ]
226 },
227 {
228 "plate": 11,
229 "propositions": [
230 {
231 "id": 29,
232 "title": "Canonical probability cone",
233 "scope": "The actual canonical behavior space is the submodule span of history/test functions from P27. Causal consistency and nonnegative behavior are supplied as CausalLaw. The all-test cone is defined by every finite test, not by finitely sampled trajectories. Cone closure under addition and nonnegative scaling, convexity, pointedness, generation by history columns, branch invariance, strict positive mass, the per-action mass identity, normalized posterior closure, and test-coordinate bounds are proved. Closedness and compact normalized-base results use the actual inherited Hausdorff function-space topology and an explicit finite-dimensional behavior-space assumption. Compactness follows through a proved closed embedding into the compact all-test unit cube; boundedness of the desired base is not assumed. The selected empty test is the literal mass-one coordinate. No finite inequality description or learned cone algorithm is claimed for the general canonical space.",
234 "modules": [
235 "KomorebiLSM/CanonicalCone.lean",
236 "KomorebiLSM/TestTopology.lean"
237 ]
238 },
239 {
240 "id": 39,
241 "title": "Finite positive-lift certificate",
242 "scope": "The cone is the actual image of nonnegative finite coefficient vectors under V. Normalization is lambda composed with V equals the coefficient-sum functional; surjectivity is the full-row-rank condition when generation is asserted. Cone closedness, convexity, pointedness, strict mass and generation are derived, including for redundant generators. The normalized base is proved equal to the image of the finite probability simplex and to the actual convex hull of the generators, and is compact. Invariance is equivalent to existence of an entrywise nonnegative matrix A with B V = V A, with the necessity witness constructed from the generator images by classical choice. Lifted mass conservation, the actual hidden instrument, intertwining for every chronological word and word probabilities follow from the finite witness and a nonnegative normalized initial coefficient vector. No unique lift is claimed for redundant V. The adjacent Farkas dual-certificate discussion is not claimed as an additional formal theorem.",
243 "modules": [
244 "KomorebiLSM/PositiveLift.lean",
245 "KomorebiLSM/PositiveLiftTopology.lean"
246 ]
247 },
248 {
249 "id": 40,
250 "title": "Robust finite-domain certificate",
251 "scope": "The uncertainty set is the actual convex hull of complete operator families with shared convex coefficients across all branches. Nonnegative vertex lifts and exact mass conservation imply every family in that hull preserves the fixed generator cone and mass. Explicit mixed lifts are constructed. History-dependent selection of a family is handled through an actual adaptive word recursion and finite observation-tree mass recursion under any deterministic history-based action policy. Cone membership, nonnegative word likelihood, the unit upper bound and tree normalization are proved for arbitrary finite horizons. A separate theorem uses actual continuous linear operators, their operator norms and a complete facet description of the same cone to prove the stated norm-ball margin implies perturbed invariance and existence of a positive lift. The normed statement specializes to Euclidean coordinates. Exact mass constraints remain separate; independently mixing branches is not inferred to conserve mass. No statistical coverage of the uncertainty hull is asserted.",
252 "modules": [
253 "KomorebiLSM/FacetRobustness.lean",
254 "KomorebiLSM/RobustFiniteDomains.lean"
255 ]
256 }
257 ]
258 },
259 {
260 "plate": 12,
261 "propositions": [
262 {
263 "id": 46,
264 "title": "A rational rank-three model with no polyhedral probability-domain certificate",
265 "scope": "The actual rational 3/5,4/5 rotation and reset-probe operators are probability valid on the Lorentz cone for every normalized state. Proves forward-orbit density, equality with the canonical all-test cone, uniqueness among closed convex conical invariant sets containing the declared initial state and admitting nonnegative mass, and no finite normalized positive-generator certificate, including redundant synthesis maps. Actual reachability and observability give predictive dimension three. A no-assumption capstone collects these results; the obstruction concerns finite polyhedral certificates, not curved or quadratic certificates.",
266 "modules": [
267 "KomorebiLSM/RotationConeGeometry.lean",
268 "KomorebiLSM/RotationDensity.lean",
269 "KomorebiLSM/RotationModel.lean",
270 "KomorebiLSM/RotationP46.lean",
271 "KomorebiLSM/RotationRank.lean"
272 ]
273 },
274 {
275 "id": 50,
276 "title": "Matrix-embedding probability certificate",
277 "scope": "An actual injective symmetric matrix embedding and positive-definite interior derive a closed, pointed, generating PSD preimage cone, strict trace mass and compact normalized base. Literal nonnegative weighted congruences, including empty sums, give branch invariance, all-word probabilities and normalized observation trees under exact mass and initial coverage. Exact atlas transport retains the witnesses. The later ambient trace-norm paragraph is separate; no automatic norm equality is claimed.",
278 "modules": [
279 "KomorebiLSM/MatrixEmbedding.lean",
280 "KomorebiLSM/MatrixOrderUnit.lean"
281 ]
282 },
283 {
284 "id": 51,
285 "title": "Exact rational matrix witness for the rotation model",
286 "scope": "The unchanged rational rotation model has the literal rational two-by-two embedding J, weight 1/5 W congruence, matrix-unit probe congruences and zero rotate branch. Derives injectivity, trace, PSD iff Lorentz, normalized disk, initial diag(1,0), definite interior and trace conservation. Every source word probability is unchanged. The P50 embedding retains P46's finite-positive-generator obstruction.",
287 "modules": [
288 "KomorebiLSM/MatrixRotation.lean"
289 ]
290 }
291 ]
292 },
293 {
294 "plate": 13,
295 "propositions": [
296 {
297 "id": 56,
298 "title": "Exact bin coarsening and its posterior",
299 "scope": "Literal Bochner cell operators preserve the cone and exact action mass. A finite measurable partition constructs a measurable bin map. Under every policy based on action/bin histories, the actual continuous record measure pushes forward exactly to the actual finite integrated-cell instrument law at every horizon; normalized initials give finite priors. The positive-cell posterior averages actual fine updates with density weights, including zero outputs. A valid 3u^2 instrument separates integration from point sampling. Within-cell-reactive policies are outside the exact coarsening claim.",
300 "modules": [
301 "KomorebiLSM/ContinuousBinnedRecords.lean",
302 "KomorebiLSM/ContinuousBins.lean"
303 ]
304 },
305 {
306 "id": 57,
307 "title": "Exact covariance correction for an averaged congruence",
308 "scope": "Finite real matrices with square-integrable entries under an actual probability measure. Derives integrability, identifies the entrywise mean with the Bochner integral, and proves the covariance identity and positive-semidefinite correction. For a scalar with finite second moment it derives the affine variance formula. Normalized Lebesgue measure on a genuine interval a<b is constructed and proved a probability measure; its variance (b-a)^2/12 and the integrated affine correction are derived.",
309 "modules": [
310 "KomorebiLSM/AveragedCongruence.lean"
311 ]
312 },
313 {
314 "id": 58,
315 "title": "Positive cell-average approximation",
316 "scope": "Actual normalized Bochner cell averages on a finite measurable positive-mass partition preserve the original cone, exact integrated mass and every cell operator. The genuine induced probability-cone base norm gives the Lh resolution bound. Actual uniform equal-interval distance integrals give Lh/3. Null/empty conventions and required finite masses, metric and Lipschitz hypotheses remain explicit; a point sample is not substituted for an integral.",
317 "modules": [
318 "KomorebiLSM/CellDistance.lean",
319 "KomorebiLSM/PositiveCellApproximation.lean",
320 "KomorebiLSM/PositiveCellP58.lean",
321 "KomorebiLSM/PositiveCellResolution.lean",
322 "KomorebiLSM/PositiveCellUniform.lean"
323 ]
324 },
325 {
326 "id": 59,
327 "title": "Continuous-record total-variation bound",
328 "scope": "Actual time-dependent Bochner DensityInstrument families on a common finite-dimensional probability cone and probability reference, with finite actions and one common measurable randomized full-history policy, have actual finite record-law TV at most min(1,(e0+sum epsilon)/2). Integrated contraction is derived from positive decompositions, and TV from the signed-measure half-density identity; no branch-density lower margin is required. The optional conditional-event helper proves an eventwise 2TV/min-masses bound with both masses positive, not the stronger adjacent full conditional-law statement.",
329 "modules": [
330 "KomorebiLSM/BaseNormIntegration.lean",
331 "KomorebiLSM/ConditionalEventTV.lean",
332 "KomorebiLSM/ContinuousTV.lean",
333 "KomorebiLSM/ContinuousTVDensity.lean",
334 "KomorebiLSM/TimeRecords.lean"
335 ]
336 }
337 ]
338 },
339 {
340 "plate": 14,
341 "propositions": [
342 {
343 "id": 72,
344 "title": "Boundary fragility under mass preserving perturbations",
345 "scope": "An actual rank-one mass-row-zero outward perturbation of exact normalized-base norm epsilon destroys a supplied boundary image, including the zero-image case.",
346 "modules": [
347 "KomorebiLSM/LorentzBoundaryFragility.lean"
348 ]
349 },
350 {
351 "id": 83,
352 "title": "Structured curved-domain certificate",
353 "scope": "The normalized curved domain equals the convex hull of moment rays; homogeneous PSD and scalar constraints define a proper full cone. Explicit four reference moments derive exact integrated mass, positivity under the declared diamond/floor condition, posterior ray and actual scalar Markov conditional moments. Both continuous and five-node references are constructed separately.",
354 "modules": [
355 "KomorebiLSM/CurvedMomentGeometry.lean",
356 "KomorebiLSM/CurvedMomentInstrument.lean",
357 "KomorebiLSM/CurvedMomentMarkov.lean",
358 "KomorebiLSM/CurvedMomentPolynomial.lean",
359 "KomorebiLSM/CurvedMomentReferences.lean"
360 ]
361 }
362 ]
363 },
364 {
365 "plate": 15,
366 "propositions": [
367 {
368 "id": 66,
369 "title": "Time-uniform predictable-residual certificate",
370 "scope": "Full arbitrary measurable probability-space time-uniform predictable residual certificate for actual conditional means, all positive times, finite/countable prospectively registered rules with literal summable budgets, exact interval-width scaling including zero width, measurable simultaneous residual/drift event, exact equivalence relabeling, and pathwise data-selected positive times/rules. No StandardBorelSpace, independence, stationarity or supplied concentration conclusion.",
371 "modules": [
372 "KomorebiLSM/ConditionalBernoulli.lean",
373 "KomorebiLSM/ConditionalHoeffding.lean",
374 "KomorebiLSM/CountableConfidence.lean",
375 "KomorebiLSM/PredictableResidualAffine.lean",
376 "KomorebiLSM/PredictableResidualAnytime.lean",
377 "KomorebiLSM/PredictableResidualGeneral.lean",
378 "KomorebiLSM/PredictableResidualP66.lean"
379 ]
380 },
381 {
382 "id": 68,
383 "title": "Sequential evidence gives a lower error certificate",
384 "scope": "Probability laws on an arbitrary measurable observation space and actual total variation defined as half the Jordan variation of their signed difference. Derives the [0,1]-test integral discrepancy bound, then the positive residual-excess lower certificate for every positive time and rule family on the stated simultaneous residual event. P66's concentration event remains a separate antecedent, exactly as in the manuscript. Noncrossing does not provide an upper law bound.",
385 "modules": [
386 "KomorebiLSM/SequentialLowerCertificate.lean"
387 ]
388 },
389 {
390 "id": 81,
391 "title": "Time-uniform regression confidence",
392 "scope": "Full finite-dimensional, all-finite-time ridge-regression confidence event under the manuscript actual conditional sub-Gaussian noise, predictable design, positive ridge/noise/budget and true-parameter norm assumptions. Arbitrary finite coordinate type and arbitrary measurable probability sample space. The formal theorem allows delta>0, extending the manuscript 0<delta<1 case with potentially trivial coverage when delta>=1.",
393 "modules": [
394 "KomorebiLSM/ConditionalRandomMultiplier.lean",
395 "KomorebiLSM/RegressionConfidence.lean",
396 "KomorebiLSM/RegressionExponential.lean",
397 "KomorebiLSM/RegressionGaussian.lean",
398 "KomorebiLSM/RegressionGeometry.lean",
399 "KomorebiLSM/RegressionRadius.lean",
400 "KomorebiLSM/ScalarRegressionConfidence.lean",
401 "KomorebiLSM/VilleInequality.lean"
402 ]
403 },
404 {
405 "id": 82,
406 "title": "Sequential observable-moment operator sets",
407 "scope": "Actual accessible history/observation joint laws give conditional posterior moments. Known invertible moment integration recovers literal coefficient matrices. Actual action-gated ridge rows and prospective finite row budgets yield simultaneous coefficient regions; exact mass intersection preserves truth; weighted directional norms retain inverse-W factors.",
408 "modules": [
409 "KomorebiLSM/ObservableMomentAlgebra.lean",
410 "KomorebiLSM/ObservableMomentConditional.lean",
411 "KomorebiLSM/ObservableMomentConfidence.lean",
412 "KomorebiLSM/ObservableMomentProcess.lean",
413 "KomorebiLSM/ObservableOperatorSets.lean"
414 ]
415 },
416 {
417 "id": 83,
418 "title": "Structured curved-domain certificate",
419 "scope": "The normalized curved domain equals the convex hull of moment rays; homogeneous PSD and scalar constraints define a proper full cone. Explicit four reference moments derive exact integrated mass, positivity under the declared diamond/floor condition, posterior ray and actual scalar Markov conditional moments. Both continuous and five-node references are constructed separately.",
420 "modules": [
421 "KomorebiLSM/CurvedMomentGeometry.lean",
422 "KomorebiLSM/CurvedMomentInstrument.lean",
423 "KomorebiLSM/CurvedMomentMarkov.lean",
424 "KomorebiLSM/CurvedMomentPolynomial.lean",
425 "KomorebiLSM/CurvedMomentReferences.lean"
426 ]
427 },
428 {
429 "id": 84,
430 "title": "Exact rational outer confidence intervals",
431 "scope": "Literal scalar ridge-one regression, sharp response-derived noise scales, integer square-root enclosure/minimality, exact dyadic log ceilings and outward endpoint prior intersections give all-time coverage for both parameters with literal failure budget1/20. No empirical coverage inference is made.",
432 "modules": [
433 "KomorebiLSM/BoundedResponseNoise.lean",
434 "KomorebiLSM/OutwardConfidenceIntervals.lean",
435 "KomorebiLSM/RationalConfidenceArithmetic.lean",
436 "KomorebiLSM/RationalRegressionConfidence.lean",
437 "KomorebiLSM/RationalSqrtEnclosure.lean",
438 "KomorebiLSM/ScalarRegressionConfidence.lean"
439 ]
440 },
441 {
442 "id": 87,
443 "title": "Observable structured learning with a covered domain",
444 "scope": "From a literal valid declared scalar conditional density and exact joint history/observation laws, derive actual conditional regression means and sharp bounded-response noise scales. The fixed predictable regressions and exact outward rational protocol yield one measurable event of probability at least19/20 covering the true parameters at every finite time. At any data-selected finite time the full returned rectangle carries actual all-horizon probability, conditional observation TV, complete-record, general geometric marginal/window and common-initial uniform bounds when its sufficient floor passes. The actual true kernel is proved equal to its certified member. No prelearning sufficient diamond, supplied confidence event, state-estimation term, independence, Standard Borel hypothesis or nominal-only domain test is introduced. Coverage remains conditional on source process/reference/prior assumptions and does not authenticate them from a path.",
445 "modules": [
446 "KomorebiLSM/StructuredLearning.lean",
447 "KomorebiLSM/StructuredLearningCapstone.lean",
448 "KomorebiLSM/StructuredRectangle.lean"
449 ]
450 }
451 ]
452 },
453 {
454 "plate": 16,
455 "propositions": [
456 {
457 "id": 85,
458 "title": "Parameter-to-law error without a state-estimation term",
459 "scope": "Actual normalized instrument-kernel measures satisfy the half-L1 parameter bound, with the posterior state exactly the observed ray. Completed history kernels equal the literal operator-product record law, giving min(1,T Delta). Discrete and continuous absolute-moment constants and final rational rectangle budget are proved. Fresh compilation exposed and repaired density equality and dependent-instance rewriting; cumulative replay remains separate.",
460 "modules": [
461 "KomorebiLSM/CurvedMomentRecordTV.lean",
462 "KomorebiLSM/CurvedMomentReferences.lean",
463 "KomorebiLSM/CurvedMomentTV.lean"
464 ]
465 },
466 {
467 "id": 86,
468 "title": "Uniform marginal and rolling-window stability",
469 "scope": "Literal measure minorization yields actual kernel contraction, its marginal recurrence and exact geometric bound including rho=1. Literal chronological records and segment pushforwards yield rolling-window budgets with entry state retained. Nondegenerate distinct iid Bernoulli laws have fixed marginal gap and full-record TV tending to one, including arbitrarily small marginal discrepancies.",
470 "modules": [
471 "KomorebiLSM/BernoulliRecordSeparation.lean",
472 "KomorebiLSM/MarkovMarginals.lean",
473 "KomorebiLSM/MarkovMinorization.lean",
474 "KomorebiLSM/MarkovRecords.lean",
475 "KomorebiLSM/MarkovWindows.lean"
476 ]
477 },
478 {
479 "id": 87,
480 "title": "Observable structured learning with a covered domain",
481 "scope": "From a literal valid declared scalar conditional density and exact joint history/observation laws, derive actual conditional regression means and sharp bounded-response noise scales. The fixed predictable regressions and exact outward rational protocol yield one measurable event of probability at least19/20 covering the true parameters at every finite time. At any data-selected finite time the full returned rectangle carries actual all-horizon probability, conditional observation TV, complete-record, general geometric marginal/window and common-initial uniform bounds when its sufficient floor passes. The actual true kernel is proved equal to its certified member. No prelearning sufficient diamond, supplied confidence event, state-estimation term, independence, Standard Borel hypothesis or nominal-only domain test is introduced. Coverage remains conditional on source process/reference/prior assumptions and does not authenticate them from a path.",
482 "modules": [
483 "KomorebiLSM/StructuredLearning.lean",
484 "KomorebiLSM/StructuredLearningCapstone.lean",
485 "KomorebiLSM/StructuredRectangle.lean"
486 ]
487 }
488 ]
489 }
490 ]
491 }
Other PDFs for this work
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: df68ebfb5a6e2a4093e22d02725b08d49671a7092ba8299eff1e3833d851737c