# Formal coverage

87 complete mappings, 0 partial and 0 unformalized. Counts are not weighted by proof difficulty.

| Proposition | Status | Mapped scope |
|---|---|---|
| P1: Exact realization and consistency | complete | 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. |
| P2: Coherent transport and operator realization | complete | 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. |
| P3: Complete refinement preserves reconstruction | complete | 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. |
| P4: Transfer reconstruction and refinement | complete | Actual linear maps between possibly different spaces, with explicit finite completeness and intermediate idempotence. The algebra works under weaker assumptions than orthogonality. |
| P5: Polynomial packet interactions | complete | All ordered multilinear interactions, including repeated packet indices. The finite polynomial sum retains every cross term. No general nonlinear dictionary discovery is claimed. |
| P6: Exact quotient criterion | complete | Reduced-map existence is constructed from fiber constancy, not assumed. Uniqueness is on the actual image, and action-indexed closure is included. |
| P7: Closure defect and compositional defect | complete | 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. |
| P8: Minimal linear predictive completion | complete | 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. |
| P9: Coarsest joint finite closure | complete | Finite state space with actual equivalence-relation partitions, known row-stochastic action kernels and positive observation likelihoods. The mandatory initial quotient is nontrivial for semantic minimality. The construction first splits by likelihood vectors, then by aggregate transition probabilities into current blocks. Strict refinements increase quotient cardinality, giving stabilization within card(states)-card(initial likelihood-split quotient) rounds; equality persists. Actual quotient kernels and positive likelihoods are constructed. Their prediction equation holds on all real vectors and their Bayesian equation on probability priors. Semantic JointlyClosed means existence of such stochastic quotient data, not an assumed structural condition. Its equivalence to lumpability plus likelihood constancy uses P12 and yields the unique coarsest admissible refinement. The exact real/setoid construction is noncomputable and does not implement a finite-precision partition learner or identify unknown dynamics. |
| P10: Exact projected memory and a conditional tail bound | complete | 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. |
| P11: Ideal statistical benefit of refinement | complete | Actual conditional expectations on nested sigma algebras. Residual orthogonality is derived from the L2 projection, giving the exact ordinary integral squared-risk identity and weak risk improvement. Holds for finite measures and complete real Hilbert targets, including the probability/finite-dimensional manuscript setting; measurability and finite second moment are explicit. |
| P12: Bayesian closure and its exact defect | complete | Finite real probability vectors and a surjective map onto the actual coarse blocks. With at least two coarse blocks and strictly positive fine and declared coarse likelihoods, commutation for every normalized nonnegative prior is equivalent to a common positive likelihood scale. Necessity is proved using two-point priors and a cross-block bridge, not assumed as fiber constancy. The one-block exception is proved separately. The effective-likelihood and matrix-defect identities include zero-prior-mass blocks. The fixed-prior algebra assumes nonnegative prior entries and nonzero fine/coarse evidences, so in particular includes nonnegative likelihoods with positive evidences. Totalized real division at zero is not interpreted as a valid posterior. Matrix null direction for a common likelihood scale is also proved. |
| P13: Strong fixed-horizon refinement limit | complete | Strong convergence is proved for actual continuous linear maps with a uniform operator bound. The compression estimate and fixed-power induction are derived. Actual orthogonal subspace projections provide the contractivity premise, for real or complex inner-product spaces. Each horizon is fixed; neither operator-norm convergence nor uniform-in-time accuracy is asserted. The fitted-operator extension retains its independent uniform-bound and strong-error assumptions. |
| P14: Exact causal delay closure | complete | 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. |
| P15: Data-span identification and its boundary | complete | 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. |
| P16: Fixed-space identification bound | complete | 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. |
| P17: Finite-prefix indistinguishability | complete | 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. |
| P18: Compositional defect propagation | complete | 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. |
| P19: Uniform prediction bound for a stable finite-memory truncation | complete | 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. |
| P20: Packet-interaction truncation bound | complete | 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. |
| P21: Coherent reconciliation and coordinate-stable transport | complete | Linear atlases act on the actual analysis-range subtype. A genuine normed additive group and normed space are constructed by pulling back synthesis; exact transports are isometries and every Lipschitz constant is equivalent to its object-space counterpart. Repaired maps are consistent and intertwine. Weighted variance and unique minimization are proved for the actual squared Frobenius objective, with a constructed orthonormal matrix coordinate equivalence in finite-dimensional real Hilbert space. The target-error inequality uses actual continuous-operator norms and nonnegative weights summing to one. Agreement is not correctness. The adjacent learned singular-value/pseudoinverse discussion is not claimed as a separate checked theorem. |
| P22: The upward-lift obstruction | complete | Existence/uniqueness between actual images, the linear kernel criterion, and the half-distance worst-case norm lower bound. An onto hypothesis in the linear-map construction means that its codomain is the true coarse state space. |
| P23: Exact accounting for an enumerated grammar | complete | Summable nonnegative whole-record grammar evidence, actual normalized posterior total variation, arbitrary bounded predictive-event kernels, exact omitted evidence and its b/(Zactive+b) bound. Includes eventual positive active evidence and actual posterior-TV convergence along every monotone exhaustive active-set sequence. The grammar is declared; no outside-grammar truth is inferred. |
| P24: Prior-preserving program refinement | complete | Arbitrary child and other-program index sets, normalized nonnegative summable priors, summable weighted likelihoods and a positive whole-record normalizer. Proves prior-mass conservation, evidence invariance, summed child posteriors, other posteriors and predictive-event equality under the separate joint-likelihood mixture. A fixed child for a whole record is distinguished from independent per-step switching. |
| P25: Observationally grounded finite linear realization | complete | Conditional finite observable realization. A covering table and true successors recover the unique map by the data-only pseudoinverse formula. Delay-range identification, every iterate, causal future output, lossless atlas recoding and complete packet synthesis are linked. The actual noisy fitted predictor feeds the product-sum error envelope, a contraction radius, and a decoder bound. Coverage and model assumptions remain supplied. No unrestricted hidden-state discovery or executable production-code verification. |
| P26: Finite instrument closure | complete | Known instrument on a finite nonempty hidden state type with finitely many outcomes. Actual nonnegative matrices obey exact per-action column-mass conservation. The P8 iteration from the nonzero mass row stabilizes within card(hidden)-1 steps and is proved equal to the span of all chronological word tests. A finite basis is extended/reindexed to place mass literally in its first coordinate. Its observation map has independent rows, is surjective onto the full coordinate space, has precisely the completed row space, and supplies unique reduced transitions. Word probabilities agree for every initial vector; probability and posterior meaning are restricted to realizableBeliefs and positive evidence. Minimality is against every linear summary with linear readouts of all words on every prior. All constructions using arbitrary real bases are noncomputable. This is not observable-data learning, minimum dimension for one fixed initialization, or a general cone-search theorem. |
| P27: Minimal finite behavior realization | complete | 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. |
| P28: Observable table reconstruction | complete | 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. |
| P29: Canonical probability cone | complete | 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. |
| P30: Positive packet decomposition and its boundary | complete | The mixture theorem works over real modules, a cone closed under nonnegative scaling, a strictly positive mass functional on nonzero cone elements, and complete linear packet maps preserving that cone. Weight nonnegativity, their unit sum, normalized component membership and mass, vanishing zero-weight components and the positive-weight finite mixture identity are proved separately. The orthant result uses actual finite real matrices: preservation of all nonnegative vectors is equivalent to entrywise nonnegativity; completeness forces zero off-diagonals; idempotence forces diagonal entries 0 or 1; every coordinate has exactly one selected packet. Reconstruction or orthogonality alone does not imply positivity. This theorem does not supply a learned cone or formalize the compactness theorem of P29. |
| P31: Missing-intervention nonidentifiability | complete | Actual one-hidden-state, two-action, two-observation stochastic instruments with a valid initial prior. Every passive observation list, including the empty list and all lengths, has common probability (1/2)^length. The missing intervention yields probabilities one and zero. Consequently the complete passive law cannot determine both unrestricted controlled laws; this is not a quantitative sample-complexity bound. |
| P32: Finite-table rank separation and subspace stability | complete | Full finite-table P32 for real finite-dimensional inner-product maps, hence rectangular real matrices with their Euclidean norms. Actual sorted, zero-padded singular values satisfy the all-index operator perturbation bound. The leading-r left subspace is constructed as images of ordered right Gram modes and proved to be the span of orthonormal left Gram modes; its dimension and exact residual norm are derived. Positive true rank and noise ≤ε<σ_r(X)/2 imply rank separation and projection gap ≤2ε/σ_r(X)<1 without supplied inverse, tail or projection-gap premises. For arbitrary orthonormal bases of the true and learned ranges, the actual cross-matrix minimum singular value is ≥sqrt(1−(2ε/σ_r(X))²), estimated coordinates are injective, and the explicit ordinary matrix inverse decoder U(UhatᵀU)⁻¹ has both inverse laws and the stated norm bound. The maximum possible rank convention is proved using zero padding. This does not certify that a finite table captures the full process. |
| P33: Noisy core-block realization | complete | Finite-dimensional real inner-product square core. The least singular value uses the inherited variational rowGain definition (infimum of adjoint norm ratios; inherited unit-sphere equivalence), consistently with P16. The constructed pseudoinverse is shown to be a two-sided inverse under the strict input error gap. Both exact error identities, the true-operator error bound, fitted-operator bound, and checked fitted-gap denominator bound are proved. Exact arithmetic and fixed core only; no data-dependent coverage or floating-point solve guarantee. |
| P34: Normalization-aware filtering stability | complete | Arbitrary real normed state space and continuous mass functional. Prediction error is derived from actual operators and states. True branch has positive mass, true state and posterior obey the supplied radius, and the strict dual-norm error budget guarantees positive fitted mass. Exact normalized residual identity and both denominator bounds are proved. Actual true and fitted recurrences yield the product-sum bound and a uniform contraction estimate. Checked realized fitted denominators do not certify all branches or probability-valid fitted states. |
| P35: Reset-experiment probability certificate | complete | Actual Hoeffding concentration for measurable bounded reset trials with common expectations and within-experiment independence. Finite nonempty experiment family, positive trial count and 0<delta<1 yield the stated radius and one simultaneous event. Explicit coverage maps transfer it to every core/shifted-block entry and initial coordinate, actual Euclidean spectral operator bounds r*epsilon and vector bound sqrt(r)*epsilon. No independence across experiments is required. |
| P36: Exact normalized closure defect | complete | The vector identity is on real coordinate functions with an actual linear summary and mass-preservation law; the fine and proposed branch evidences are strictly positive. The separate likelihood identity holds without division. The oblique map is an actual rank-one correction of the identity. The converse requires a nonzero entrywise-nonnegative fine branch and agreement of likelihoods AND normalized posteriors on every strictly positive prior. Explicit uniform and perturbed-uniform priors prove that this interior family spans the fine space. No equality of unnormalized operators is assumed in that converse. A one-state instrument counterexample proves that posterior agreement alone is insufficient. The idempotent-projector specialization gives the omitted-to-retained block. The statements do not certify a fitted probability domain or control statistical error. |
| P37: Conditional observation-based stochastic completion | complete | Actual causal behavior law, finite-dimensional behavior space, invertible covered core containing the empty test and the stated rank bound. Constructs the canonical cone in observable coordinates, exact all-word minimal realization and positive-history updates. Proves arbitrary invertible atlas state/operator/mass/cone transport and full packet readout. The actual sampled blocks yield simultaneous spectral and operator certificates on the same reset event with the original failure budget; filtering retains state bounds, core/spectral gaps and branch likelihood margins. Estimated-model positivity is not inferred. |
| P38: Test-cone hierarchy and a finite stopping certificate | complete | The finite-level cones are actual inequalities for all words of length at most h. Their successor/preimage identity, antitonicity, intersection, largest invariant-set property and exact adjacent-level stopping implication are proved. A noncomputable finite set of linear halfspaces is constructed at every level for finite symbol types, establishing the polyhedral description rather than assuming it. An observability row-span hypothesis is connected to injectivity of all-test evaluation. With the explicit per-action mass law, injectivity yields pointedness and strictly positive mass; membership of reachable vectors and their full span yields generation. Finite stabilization is sufficient, not asserted for every family. A one-step acceptance test is not treated as invariance. The cone may be improper without the stated observability/reachability conditions. |
| P39: Finite positive-lift certificate | complete | 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. |
| P40: Robust finite-domain certificate | complete | 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. |
| P41: Certified correction and its error budget | complete | A FeasiblePoint records the actual finite nonnegative-lift, intertwining, per-action mass and initial-prior constraints. Internal family validity, normalized initial membership and every finite-word probability are derived from those constraints and normalized generators, not included as assumed conclusions. An actual true member of a confidence set with a fixed-domain witness constructs a feasible point in that set. The two-center bound norm(corrected-truth) <= 2 epsilon is proved for an arbitrary seminormed additive group, hence applies both to continuous linear operators and to initial states in their specified norms. No optimizer, empirical confidence set, or implication from one feasible point to coverage/validity of every point is supplied. Fixed-domain witness construction is classical and noncomputable. The adjacent explicit mixing-repair formula is outside this numbered proposition's mapping. |
| P42: Instrument contraction before normalization | complete | The base norm is the actual infimum over decompositions x=u-v with u,v in the declared closed, generating cone. Nonnegative mass, existence of decompositions, the infimum bounds, triangle inequality, negation invariance and absolute scalar homogeneity are proved. In finite-dimensional real normed spaces, compactness of the normalized base and a bound by the ambient norm are derived from cone closedness and strict mass; nondegeneracy supplies an actual AddGroupNorm, not an assumed norm. Instrument means cone preservation and exact total mass, not assumed contraction. Summed contraction is proved by the positive-decomposition infimum. For a normalized base equal to a nonempty finite convex hull, the discrepancy supremum is attained at a generator. For two valid instruments it is at most two. The finite positive-lift domains of the previous block instantiate this construction. Invertible synthesis gives the inverse-coordinate l1 formula; redundant synthesis gives only an upper bound for any chosen signed coefficients. The adjacent convex-hull unit-ball identity and general LP minimum-attainment assertion are not separately mapped as additional results. These are noncomputable exact real constructions, not a numerical norm minimizer. |
| P43: Observation-tree total-variation bound | complete | The record space, chronological history update, unnormalized record states, record probabilities and total mass are constructed explicitly for each finite horizon. The summed base-norm error is proved by induction, not assumed as a recurrence conclusion. The actual finite total variation is half the sum of absolute probability differences. Arbitrary shared history-dependent branch families, and shared deterministic or randomized history-dependent action policies over finite alphabets, are covered. Complete per-action instruments are multiplied by the same policy probabilities in the two compared models. Joint action/observation laws are proved normalized; observation-only laws are their actual aggregation and inherit the bound. The P42 all-state discrepancy supremum supplies the pointwise budget. The bound retains the initial-state discrepancy and sum of per-time budgets, with min(1, ...) clipping. No positive lower branch likelihood or action propensity is assumed. The norm, cone, mass row, observation alphabet and policy are common. No comparison of separately optimized or different policies, infinite-horizon accuracy, continuous observations or learned statistical coverage is claimed. |
| P44: Sharp event-probability dependence of conditioning | complete | Finite distributions are actual nonnegative normalized real vectors. Event restriction, event mass and normalized conditional distribution are defined by finite sums. The exact restriction/complement budget and event-mass difference bound are proved. For strictly positive event masses in both laws, conditioning has total variation at most min(1, delta/true_event_mass). If delta is strictly below the true event mass, positivity in the comparison law is derived, not assumed. Aggregating conditional records also obeys the bound. The factor is sharp for every 0<r<=1 and 0<=d<=r, using explicit three-state priors with common event mass r, unconditional distance d and conditional distance d/r. A concrete impossible-event expression is not treated as a prior. No bound independent of event mass or general measure-theoretic conditioning is claimed. |
| P45: Rational finite-certificate search | complete | Finite rational input matrices and exact per-action mass identities. The input certificate only assumes rational normalized full-row-rank generators; its nonnegative lift and initial coefficients may be real. Finite weak rational Fourier–Motzkin elimination proves rational witnesses exist, including boundary faces. A rational right inverse is derived. Computable natural-number decoding enumerates every finite width and rational witness, exact rational checks are sound, and some finite fuel returns a certificate whenever the stated one exists. Accepted witnesses instantiate the closed, pointed, generating invariant cone and all-word bounds of P39. No strict margin, practical complexity, universal existence, or finite-failure impossibility is claimed. |
| P46: A rational rank-three model with no polyhedral probability-domain certificate | complete | 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. |
| P47: Polyhedral approximation of the rotation model | complete | The actual regular n-gon, n>=3, has the derived cosine inradius and normalized full-row-rank vertex synthesis. For 0<=alpha<=cos(pi/n), constructs nonnegative intertwining matrices, exact action mass, a covered initial prior and all-word equality. Derives the actual Lorentz base norm from its positive-decomposition infimum, and the observation-law bound min(1,T(1-alpha)/2) for every common randomized history-dependent policy. The rational diamond works for alpha<=5/7, including entirely rational certificate data at 2/3. The explicit max(3,ceil(pi/sqrt(2 eta))) bound yields a certificate for 0<eta<=1. Exact rational probabilities prove that attenuation changes the law. |
| P48: Sequential confidence accounting for certified proposals | complete | Actual conditional expectations of measurable failure indicators imply unconditional stage bounds. A summable countable prospective budget gives one measurable all-stage coverage event with probability at least 1-delta. On that event, deterministic robust soundness over the entire returned uncertainty set applies to the true member when the initial base is covered; every selected or stopped stage inherits the conclusion. Validity is interpreted through the measurable simultaneous coverage event, without a new measurability assumption on an arbitrary validity predicate. |
| P49: Conditional learning with an all-horizon probability certificate | complete | Actual P37 observable population-table reconstruction under the declared covered invertible core and rank bound, combined with P39 normalized full-row-rank finite synthesis and literal nonnegative matrix/prior witnesses. Derives internal all-word probability validity, a common true/fitted finite-cone instrument domain with covered initials under robust whole-set coverage on a supplied measurable event, including a finite domain chosen from the data, and both full-record and observation-law common-policy TV bounds min(1,(e0+sum epsilon)/2). Finite robust vertex checks construct whole-set witnesses. Reachability also derives surjectivity for a true observable-model witness. Conditioning retains positive true and fitted event masses. Exact atlas transport preserves the same coefficient matrices and prior. Complete signed-packet synthesis preserves every word prediction; probability mixtures and individual normalized packet states retain separate cone positivity. Statistical coverage is an antecedent supplied by the observation protocol, not inferred from fitting. |
| P50: Matrix-embedding probability certificate | complete | 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. |
| P51: Exact rational matrix witness for the rotation model | complete | 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. |
| P52: Continuous-observation instrument semantics | complete | Actual Bochner-integrable operator densities, whole-cone positivity outside a common null set and exact integrated mass construct Markov kernels and jointly measurable normalized updates with fixed valid fallback. Actual operator-product record measures are normalized and prefix-consistent under arbitrary measurable randomized history policies, with the proved kernel/update compProd bridge. Prescribed actions have the exact product-reference density. Positive normalized reference rescaling r mu with B/r preserves kernels, updates almost everywhere and full finite record laws. |
| P53: Polynomial Gram certificate for interval observations | complete | Literal output/input Choi indexing and spectral factors derive positive congruence maps from PSD matrices. Actual interval power-stack Gram witnesses prove whole-interval positivity, including degree zero. Finite coefficient checks on a genuine basis imply full intertwining; actual uniform moments and Bochner integration check mass. The aggregate uses the actual P50 embedding/interior and constructs the P52 instrument, positive-density updates and all-horizon probability/consistency/product-density semantics. This is a sufficient certificate, not a completeness theorem. |
| P54: Conditional finite-moment identification | complete | Genuine normalized uniform moments and positive squared integrals of nonzero polynomials derive Gram invertibility. A covered square population core in the supplied true dimension gives exact moment/coefficient reconstruction, the entire polynomial density and all word coordinates. Error uses one fixed induced norm. Actual bounded signed reset trials give the range-two simultaneous radius with positive counts, 0 < delta < 1, exact expectations and within-entry independence. Rank, degree, coverage and resets remain premises; event/table integral dictionaries are explicit. |
| P55: A valid continuous counterexample to finite-moment identification | complete | Actual cubic Legendre densities 1 +/- epsilon L3 for 0 < epsilon < 1 are strictly positive and normalized with equal moments 0,1,2. Genuine integration gives integral /L3/ = 13/40 and actual measure TV = 13epsilon/40, hence distinct laws. Independent finite product laws share every low-order product moment at all lengths. Actual scalar event realization and integral dictionaries give rank-one event Hankel matrices containing empty experiments. Nonzero perturbations are outside the quadratic class. |
| P56: Exact bin coarsening and its posterior | complete | 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. |
| P57: Exact covariance correction for an averaged congruence | complete | 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. |
| P58: Positive cell-average approximation | complete | 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. |
| P59: Continuous-record total-variation bound | complete | 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. |
| P60: Exact recognition of a fixed certified template | complete | Literal fixed-template coefficient/mass matching is a finite real linear system. Fitted coefficient-word observability derives uniqueness among all linear matches, including singular competitors. An invertible match transports the actual matrix-domain polynomial Gram certificate with unchanged Gram data, exact mass and actual finite record laws. Fitted initial PSD and mass normalization remain a separate check. Observability neither supplies invertibility nor guarantees existence. |
| P61: Conditional continuous realization with a finite domain certificate | complete | Actual supplied finite dimension and polynomial degree with an invertible complete population core derive inverse-moment fitted coefficients, full densities and word likelihoods. The independent P53 finite matrix/Gram/moment witness and transformed initial PSD/mass check for that same family yield actual all-horizon laws. Literal original/atlas event-law transport, a sufficient invertible P60 template constructor, complete signed synthesis with separate packet positivity, actual bin-policy pushforward, P58 Lh and Lh/3 resolution and P59 common-cone/reference/policy budgets are connected to the same fitted instrument. No dimension/degree discovery, empirical coverage or generating-process adequacy is inferred. |
| P62: Oriented quadratic probability certificate | complete | Actual positive-definite metric and centered mass coordinates derive a genuine curved ProbabilityCone, including empty spatial dimension. Literal Q, PSD remainder and nonnegative multiplier plus both inverse-metric orientation inequalities imply cone preservation. Finite interval SOS/Gram/degree/coefficient and exact moment checks construct the actual uniform-reference polynomial DensityInstrument and arbitrary-policy probability laws, word densities and prefixes at every horizon. This is a sufficient replayable certificate, not a completeness result for search. |
| P63: Conditional operator-only ellipsoid discovery | complete | The literal fitted polynomial ratio, its invertibility and mass row derive the affine block form and unique fixed center. An actual one-dimensional symmetric invariant-form subspace with a positive-definite member, and an actual rank-one fitted anchor with nonzero normalized displacement, derive the unique normalized positive metric. Complete P62 witnesses, exact mass and initial coverage for the same fitted family then yield actual all-horizon laws. Boundary placement remains a conditional proposal; failed discovery does not prove invalidity. |
| P64: Valid positive polynomial approximation | complete | Literal Bernstein-Durrmeyer integral coefficients define cone-positive degree-at-most-n polynomial operators with exactly unchanged integrated mass. The actual doubly stochastic kernel has squared displacement 1/(3(n+2)); its actual joint-law variance inequality gives integrated genuine base-norm error L/sqrt(3(n+2)) under the stated induced-norm Lipschitz premise. Actual common-policy record laws obey min(1,TL/(2sqrt(3(n+2)))). No finite true-degree assumption is imposed; adjacent scalar examples are separate. |
| P65: Certified coefficient error and approximation bias | complete | Actual fitted positive Bernstein coefficients with exact average mass define a genuine DensityInstrument and finite policy probability laws. Normalized-input genuine base-norm coefficient budgets integrate to their average; the finite-action maximum is added to the actual P64 L/sqrt(3(n+2)) approximation bias. A separately supplied actual correction discrepancy is added by a proved integral triangle inequality. Positivity and mass alone do not erase coefficient error. |
| P66: Time-uniform predictable-residual certificate | complete | 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. |
| P67: Covered adaptive-action evidence | complete | Full countable-rule, every-positive-time contextual inverse-propensity concentration from an actual action/observation joint-law factorization. |
| P68: Sequential evidence gives a lower error certificate | complete | 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. |
| P69: Observation-law error without a shared state space | complete | Actual causal joint action/observation record-law TV bounded by initial TV plus expected-under-P conditional TV costs, capped by one. |
| P70: Separate structural acceptance, approximation control and sequential rejection | complete | Compositional full P70 conjunction of separately assumed structural, approximation, causal-kernel, sequential and covered-action implications. New explicit bridges derive exact P62 all-horizon validity, P64-P65 common-domain full-law upper control, and P66-to-P68 simultaneous measurable actual-law lower evidence with AE true conditional means. P63 proposal, P67 contextual coverage and P69 outside-representation comparisons retain their exact hypotheses. Structural acceptance and nonrejection imply no upper accuracy or generating model-class membership. Different observation reference measures are never silently identified. |
| P71: Robust oriented margin | complete | Attained minimum over the full normalized Lorentz base gives the exact robust margin and an actual polynomial density instrument in an arbitrary mass-preserving atlas. |
| P72: Boundary fragility under mass preserving perturbations | complete | 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. |
| P73: Interior repair with an explicit error budget | complete | Literal center-reset mixture derives its slack, robust preservation, integrated cost (1-eta)*epsilon+2*eta, and actual common-policy probability-TV law bound. |
| P74: A posteriori proposal error | complete | Actual invariant-form/trace map with Frobenius domain and Euclidean product range yields the singular-gap residual estimate, matrix perturbation budget and fixed-center estimate. |
| P75: Rational semicircle and Bernstein certificate | complete | Literal rational two-chart polynomials plus complete binary subdivision prove full disk margin; actual coefficient convergence proves eventual dyadic success under strict actual margin. |
| P76: Coefficient boxes and convex uncertainty | complete | Actual degree-wise matrix-entry boxes imply mass/spatial budgets 3*sum r and 6*sum r; convex complete-family and initial-state hulls retain the full-domain margin and mass. |
| P77: Conditional search for strict rational curved certificates | complete | Strict real finite sector yields an actual rational mass-preserving invertible transform, finite rational Bernstein witnesses and eventual return of an explicit encoded first-valid scan, with original-coordinate convex-hull soundness. |
| P78: Data-selected geometry with honest coverage | complete | Pointwise selection from the same covered uncertainty set certifies the selected domain; exact whole-state Euclidean norm calculations give transformed output budget 2*norm(T)*norm(T inverse)*e. |
| P79: Certified repair with a retained comparison budget | complete | Literal rational Section88 perturb-and-reset fixtures are tied to both inverse atlases. All sixteen submitted orientation and square-gap complete subdivision witnesses construct nominal instruments in the proposed and comparison domains. Exact integrated mass, the physical initial center, all-horizon nominal and mass-constrained uncertain laws, the retained 3/64 robust slack, actual degree-two 1/4096 coefficient-box inclusion, the literal one-eighth reset identity, exact 81687/320000 integrated budget and 81687*N/640000 common-policy TV budget are connected in one module. |
| P80: Convex repair bracketing | complete | Actual full-domain feasible repair weights form the closed interval [etaStar,1]; an evaluated cone-positive row gives the ratio lower cut and a genuine complete Bernstein certificate gives the upper cut. |
| P81: Time-uniform regression confidence | complete | 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. |
| P82: Sequential observable-moment operator sets | complete | 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. |
| P83: Structured curved-domain certificate | complete | 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. |
| P84: Exact rational outer confidence intervals | complete | 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. |
| P85: Parameter-to-law error without a state-estimation term | complete | 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. |
| P86: Uniform marginal and rolling-window stability | complete | 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. |
| P87: Observable structured learning with a covered domain | complete | 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. |