| OCP-001 |
Formal OCP tuple |
An OCP system can be formalized as a protected/disturbance/correction tuple with exact and asymptotic branches. |
PROVED |
repo-local definition and consistency checks |
High |
docs/formalism/formal-theory.md |
Use as the primary formal language. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-002 |
Exact orthogonal projection theorem |
If H = S ⊕ D with S orthogonal to D, orthogonal projection onto S exactly recovers the protected component of any state s+d. |
PROVED |
linear-algebra proof and tests |
High |
docs/theorem-candidates/central-theorem.md; tests/math/test_core_projectors.py |
Promote as the clean finite-dimensional backbone. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-003 |
Indistinguishability no-go |
If S ∩ D is nontrivial, no single-valued recovery map can recover s from x=s+d for all s in S and d in D. |
PROVED |
elementary contradiction proof |
High |
docs/impossibility-results/no-go-results.md |
Promote as the strongest exact no-go statement. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-004 |
Continuous damping theorem |
The flow xdot = -k P_D x leaves S fixed and exponentially suppresses D. |
PROVED |
closed-form solution and tests |
High |
docs/theorem-candidates/backup-theorems.md; tests/math/test_core_projectors.py |
Use as the bridge from exact correction to asymptotic correction. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-005 |
QEC exact anchor |
Knill-Laflamme style exact correction fits OCP when syndrome sectors are orthogonal and recoverable. |
CONDITIONAL |
standard QEC theorem plus repo-local rewrite |
High |
docs/qec/qec-in-ocp.md; tests/math/test_qec_knill_laflamme.py |
Keep exact but conditional on KL-type assumptions. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-006 |
Helmholtz/Leray exact continuous anchor |
Periodic Helmholtz projection gives an exact OCP recovery operator for divergence-free fields under additive gradient contamination. |
PROVED |
FFT operator construction and tests |
High |
docs/mhd/divergence-cleaning-in-ocp.md; tests/math/test_mhd_projection.py |
Promote heavily as the best exact continuous example. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-007 |
GLM as asymptotic OCP |
GLM divergence cleaning fits OCP as an asymptotic correction architecture rather than an exact projector. |
CONDITIONAL |
implementation analysis and empirical reduction tests |
Medium |
docs/mhd/glm-and-asymptotic-correction.md; tests/examples/test_glm_decay.py |
Present as a good asymptotic example, not exact correction. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-008 |
Control-theoretic instantiation |
Observer/controller designs instantiate OCP when the protected/disturbance split is invariant and feedback acts only on disturbance coordinates. |
CONDITIONAL |
structural control analysis |
Medium |
docs/control/control-extension.md |
Keep conditional and design-oriented. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-009 |
Universal scalar correction capacity |
There exists one scalar correction-capacity number that nontrivially classifies QEC, MHD projection, GLM, and control architectures. |
OPEN |
failed unification attempt |
Low |
NOVELTY_AND_LIMITS.md; docs/impossibility-results/no-go-results.md |
Do not promote without a better category-specific definition. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-010 |
Topological Adam / ML extension |
Current optimizer work is a genuine OCP instantiation rather than a loose bridge. |
ANALOGY ONLY |
local sibling-repo evidence is too weak |
Low |
docs/disproven-or-weak/weak-extensions.md |
Keep secondary and unpromoted. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-011 |
Engineering design value |
OCP yields practical design rules for building correction operators and recognizing when a correction architecture is underpowered. |
CONDITIONAL |
operator examples and no-go criteria |
Medium |
docs/applications/practical-use-cases.md |
Use as the main practical pitch, but keep the domain assumptions explicit. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-012 |
Exact-to-asymptotic bridge |
OCP gives a meaningful bridge between discrete exact correction and continuous asymptotic correction. |
CONDITIONAL |
formalism + exact and asymptotic branches |
Medium |
docs/formalism/exact-vs-asymptotic.md |
Promote after upgrading the bridge from framework language to a sharper theorem statement. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-013 |
Invariant-split generator theorem |
If K annihilates S, preserves D, and its restriction to D is exponentially stable, then the flow xdot=-Kx preserves S and asymptotically suppresses D. |
PROVED |
linear ODE proof and tests |
High |
docs/theorem-candidates/generator-theorems.md; tests/math/test_continuous_generators.py |
Promote as the strongest next-step theorem beyond the projector case. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-014 |
Self-adjoint PSD corollary |
If K is self-adjoint positive semidefinite with ker(K)=S and spectral gap lambda_*>0 on S^perp, then |
|
e^{-tK}x-P_S x |
|
<= e^{-lambda_* t} |
|
P_D x |
|
. |
PROVED |
spectral proof and tests |
High |
docs/theorem-candidates/generator-theorems.md; tests/math/test_continuous_generators.py |
Use as the cleanest grounded continuous-time strengthening. |
|
|
|
|
| OCP-015 |
Mixing no-go for linear flows |
If P_S K P_D is nonzero, then disturbances generically leak into the protected coordinates and the flow is not an OCP correction flow preserving S pointwise. |
PROVED |
derivative-at-zero argument and tests |
High |
docs/impossibility-results/no-go-results.md; tests/math/test_continuous_generators.py |
Promote as the strongest new linear-flow failure criterion in the repo. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-016 |
Exact correction rank lower bound |
For an exact linear recovery on V = S ⊕ D with correction operator C = I - R, one must have rank(C) >= dim(D) and rank(R) >= dim(S). |
PROVED |
linear-algebra proof and tests |
High |
docs/theorem-candidates/capacity-theorems.md; tests/math/test_capacity.py |
Promote as the cleanest minimum-structure theorem in the repo. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-017 |
Sector distinguishability lower bound |
Pairwise orthogonal nonzero exact-correction sectors require at least as many distinguishable correction labels as sectors. |
CONDITIONAL |
sector-based argument plus QEC example |
Medium |
docs/theorem-candidates/capacity-theorems.md; tests/math/test_capacity.py |
Keep this branch-specific and avoid overstating it beyond the exact sector model. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-018 |
Category-specific capacity view |
OCP supports branch-specific correction-capacity notions even though a universal scalar capacity remains unsupported. |
CONDITIONAL |
definitions, lower bounds, and examples across branches |
Medium |
docs/theorem-candidates/capacity-theorems.md; docs/open-questions/viable-next-directions.md |
Develop this further before treating it as a mature theory. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-019 |
Exact sector recovery theorem |
Pairwise orthogonal coordinate-compatible disturbance sectors admit an exact sector-conditioned recovery operator mapping each sector back to the protected space. |
PROVED |
operator construction, proof sketch, and tests |
High |
docs/theorem-candidates/sector-recovery-theorems.md; tests/math/test_sector_recovery.py |
Promote as the finished exact sector branch beyond the simple projector model. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-020 |
Finite-time exact recovery no-go for smooth linear flows |
If D is nontrivial, a finite-time linear flow e^{-tK} cannot satisfy Φ_t(s+d)=s for all s in S, d in D at any finite t>0. |
PROVED |
invertibility argument plus workbench and test examples |
High |
docs/impossibility-results/advanced-no-go-results.md; tests/math/test_continuous_generators.py |
Use this as the sharp separator between exact recovery and asymptotic linear correction. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-021 |
Sector-overlap detection no-go |
If two candidate disturbance sectors overlap nontrivially, exact unique sector detection is impossible on the shared family. |
PROVED |
subspace contradiction proof and overlapping-sector test case |
High |
docs/impossibility-results/advanced-no-go-results.md; tests/math/test_sector_recovery.py |
Promote as the sector-branch analog of the overlap no-go. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-022 |
Transverse gauge projection fit |
On projection-compatible domains, Coulomb-gauge or transverse-field projection is an exact protected-state correction fit by the same projector logic as the Helmholtz/Leray branch. |
PROVED ON SUPPORTED FAMILY |
direct corollary of the projection branch plus physics reinterpretation |
Medium |
docs/physics/maxwell-coulomb-gauge.md; docs/mhd/divergence-cleaning-in-ocp.md |
Keep as a physics extension, not as a novel operator theorem. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-023 |
Periodic projector transplant to bounded domains |
The periodic exact projector can be reused unchanged as an exact bounded-domain correction operator preserving the bounded protected class. |
DISPROVED |
explicit boundary counterexample and tests |
High |
docs/physics/bounded-domain-projection-limits.md; tests/examples/test_bounded_domain_projection_limit.py |
Use as the clearest physics-side rejection of naive projector transplantation. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-024 |
Constraint damping in additional physics systems |
Constraint damping architectures in systems such as numerical relativity fit the asymptotic OCP branch when a protected/constraint-violation split and a stable correction generator are made explicit. |
CONDITIONAL |
cross-system operator comparison |
Medium |
docs/physics/numerical-relativity-constraint-damping.md; docs/mhd/glm-and-asymptotic-correction.md |
Keep as a viable physics extension and future application lane. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-025 |
Continuous quantum error correction bridge |
Continuous quantum error correction and feedback architectures fit the asymptotic or measurement-conditioned OCP branches when syndrome information remains sufficiently distinguishable and feedback preserves the code sector. |
CONDITIONAL |
QEC/control literature comparison plus branch mapping |
Medium |
docs/physics/continuous-quantum-error-correction.md; docs/qec/qec-in-ocp.md |
Keep as a citable future bridge, but do not promote it as a proved new theorem. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-026 |
Generic constrained Hamiltonian fit |
Generic constrained Hamiltonian systems automatically determine a nontrivial OCP correction architecture. |
ANALOGY ONLY |
current repo lacks a canonical projector/recovery construction in that generality |
Low |
docs/physics/kept-vs-rejected-physics-bridges.md |
Do not promote without an explicit reduction or correction operator. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-027 |
Periodic incompressible projection fit |
Periodic incompressible velocity projection is an exact protected-state correction fit by the same Helmholtz/Hodge projector logic as the exact continuous branch. |
PROVED ON SUPPORTED FAMILY |
operator corollary plus executable periodic CFD tests |
High |
docs/cfd/incompressible-projection.md; docs/theorem-candidates/cfd-projection-results.md; tests/math/test_cfd_projection.py |
Keep as the narrow strongest CFD extension. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-028 |
Divergence-only bounded recovery no-go |
On a nontrivial bounded incompressible protected class, any recovery map that factors only through the divergence scalar field cannot be an exact recovery operator. |
PROVED |
elementary distinguishability argument plus bounded-state witness |
High |
docs/cfd/bounded-vs-periodic-projection.md; docs/theorem-candidates/cfd-projection-results.md; tests/math/test_cfd_projection.py |
Promote as the sharp CFD-facing limitation theorem. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-029 |
Bounded-domain projection classification |
Bounded-domain incompressible projection belongs to the exact branch only when the correction step realizes the domain-compatible Hodge projector for the actual protected class and boundary data. |
CONDITIONAL |
classification statement tied to the bounded counterexample and Hodge-projector criterion |
Medium |
docs/cfd/helmholtz-hodge-velocity-projection.md; docs/cfd/cfd-system-matrix.md; docs/physics/bounded-domain-projection-limits.md |
Keep this conditional until a full bounded-domain operator theorem is proved. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-030 |
Observation fiber exactness |
A protected variable is exactly recoverable from a constrained record map if and only if it is constant on the record fibers; equivalently κ_{M,p}(0)=0. |
PROVED |
formal derivation plus branch tests |
High |
docs/theory/advanced-directions/constrained-observation-formalism.md; docs/theorem-candidates/constrained-observation-theorems.md; tests/math/test_recoverability.py |
Keep as the backbone of the constrained-observation branch, but do not market it as a novelty claim by itself. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-031 |
Restricted linear protected-variable recovery |
For x = Fz, M(x)=Ox, and p(x)=Lx on a finite-dimensional family, exact linear protected-variable recovery exists if and only if ker(O F) is contained in ker(L F). |
PROVED |
linear-algebra derivation and tests |
High |
docs/theory/advanced-directions/constrained-observation-formalism.md; docs/theorem-candidates/constrained-observation-theorems.md; tests/math/test_recoverability.py |
Use as the main exact bridge to observability and restricted recovery. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-032 |
Fixed-basis phase-loss no-go |
A fixed computational-basis record cannot exactly recover a phase-sensitive protected variable on a qubit family that contains the same amplitudes with varying phase, even though weaker protected variables such as the z coordinate remain recoverable. |
PROVED |
toy-model derivation and computational sweep |
Medium |
docs/impossibility-results/constrained-observation-no-go.md; docs/theory/advanced-directions/constrained-observation-results-report.md; tests/math/test_recoverability.py |
Keep as the cleanest quantum-side no-go inside the branch. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-033 |
Periodic record classification |
On the tested periodic incompressible family, full vorticity is an exact protected-variable record, truncated vorticity is approximate only, and divergence-only observation is a no-go. |
CONDITIONAL |
conventional computational benchmark with generated artifacts |
Medium |
docs/theory/advanced-directions/constrained-observation-results-report.md; data/generated/recoverability/recoverability_summary.json; tests/math/test_recoverability.py |
Keep as a strong computational result, but do not overstate it beyond the tested family. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-034 |
Finite-history versus asymptotic recovery split |
In the two-state scalar-output control toy model, one-step exact recovery fails, two-step protected-variable recovery is exact whenever ε(a-b) ≠ 0, and observer-based asymptotic recovery still converges from the ongoing record. |
PROVED |
model-specific derivation, explicit formula, and computational sweep |
Medium |
docs/theory/advanced-directions/constrained-observation-derivations.md; docs/theory/advanced-directions/constrained-observation-results-report.md; tests/math/test_recoverability.py |
Keep as the branch’s clearest exact-versus-asymptotic observation example, but only at the toy-model level. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-035 |
Collapse-modulus noise lower bound |
For any estimator receiving records with adversarial observation error at most η, the worst-case protected-variable error is bounded below by κ_{M,p}(η)/2. |
PROVED |
metric derivation plus analytic benchmark and tests |
High |
docs/theory/advanced-directions/constrained-observation-derivations.md; docs/theorem-candidates/constrained-observation-theorems.md; tests/math/test_recoverability.py |
Promote as the strongest operational theorem currently supporting the κ branch. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-036 |
Restricted observation rank lower bound |
On a finite-dimensional admissible linear family x=Fz with record OFz and protected variable LFz, exact protected-variable recovery implies rank(OF) >= rank(LF). |
PROVED |
rank-nullity derivation and tests |
Medium |
docs/theory/advanced-directions/constrained-observation-derivations.md; docs/theorem-candidates/constrained-observation-theorems.md; tests/math/test_recoverability.py |
Keep as a branch-specific minimum-record lower bound without reviving the old universal-capacity idea. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-037 |
Qubit phase-window collision law |
For the fixed-basis qubit record on the phase-window family φ ∈ [-w,w], the full Bloch-vector fiber ambiguity satisfies κ(0)=2 sin(min(w, π/2)); exact full recovery holds only at w=0, while weaker protected variables such as z remain exactly recoverable. |
PROVED |
closed-form derivation and numerical sweep |
Medium |
docs/theory/advanced-directions/constrained-observation-derivations.md; docs/theory/advanced-directions/constrained-observation-results-report.md; tests/math/test_recoverability.py |
Keep as the cleanest family-level phase-transition law in the branch. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-038 |
Periodic cutoff threshold on the two-mode family |
For the tested two-mode periodic incompressible family, truncated-vorticity recovery is exact if and only if the Fourier cutoff retains both active modes, which first occurs at cutoff 2. |
PROVED |
family-level rank argument plus recovery-error sweep |
Medium |
docs/theory/advanced-directions/constrained-observation-derivations.md; docs/theory/advanced-directions/constrained-observation-results-report.md; tests/math/test_recoverability.py |
Promote as a narrow but real coarsening threshold result and keep it explicitly family-specific. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-039 |
Periodic functional-support threshold |
On the tested four-mode periodic incompressible modal family, exact recovery of a protected linear functional from truncated vorticity is possible if and only if the cutoff retains every Fourier mode used by that functional; the minimal exact cutoff therefore equals the largest protected mode cutoff. |
PROVED |
kernel-based derivation, row-space residual checks, discretization checks, and recovery sweeps |
Medium |
docs/theory/advanced-directions/constrained-observation-derivations.md; docs/theorem-candidates/constrained-observation-theorems.md; docs/theory/advanced-directions/constrained-observation-results-report.md; tests/math/test_recoverability.py |
Promote as the branch’s strongest current periodic minimal-record threshold law, but keep it family-specific. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-040 |
Nested linear minimal observation complexity |
For a nested finite-dimensional linear observation family x=Fz with records O_r F z and protected variable L F z, exact recovery turns on at the first level r for which row(L F) is contained in row(O_r F). |
PROVED |
restricted-linear derivation plus independent periodic/control threshold checks |
Medium |
docs/theory/advanced-directions/constrained-observation-derivations.md; docs/theorem-candidates/constrained-observation-theorems.md; tests/math/test_recoverability.py |
Keep as the cleanest current generalization of the branch’s family-level threshold laws. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-043 |
Nested restricted-linear collision-gap threshold law |
On the bounded coefficient family A_B = {F z : |
|
z |
|
_∞ ≤ B}, the structured collision gap Γ_r(B) is monotone along nested record families, vanishes exactly at the first exact-recovery level, and yields a zero-noise lower bound Γ_r(B)/2 below threshold. |
PROVED |
restricted-linear derivation, independent nullspace-on-a-box checks, stress sweeps, and generated-artifact consistency tests |
High |
docs/theory/advanced-directions/constrained-observation-formalism.md; docs/theory/advanced-directions/constrained-observation-derivations.md; docs/theorem-candidates/constrained-observation-theorems.md; tests/math/test_recoverability.py; tests/examples/test_generated_artifact_consistency.py |
Promote as the branch’s strongest current theorem-grade threshold result, but keep it explicitly within the restricted linear setting. |
|
|
|
|
|
|
|
|
| OCP-041 |
Same-record weaker-versus-stronger split |
A fixed coarse record can exactly recover a weaker protected variable while exact recovery of a stronger protected variable remains impossible whenever the weaker protected row lies in the observation row space and the stronger one does not. |
PROVED |
row-space argument plus periodic/control counterexample families |
Medium |
docs/theory/advanced-directions/constrained-observation-derivations.md; docs/theory/advanced-directions/constrained-observation-clean-results.md; tests/math/test_recoverability.py |
Promote as a useful negative result and organizing principle without overselling it as a broad new theory. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-042 |
Diagonal functional interpolation threshold |
In the tested scalar-output diagonal family with distinct active eigenvalues, exact recovery of a protected linear functional g·x_0 is possible at horizon H if and only if g_j / c_j agrees on the active sensor spectrum with a polynomial of degree at most H-1, with hidden protected directions remaining impossible; the coordinate threshold is a special case. |
PROVED |
Vandermonde/interpolation derivation plus independent linear-recovery, nullspace, and sweep tests |
Medium |
docs/theory/advanced-directions/constrained-observation-derivations.md; docs/theorem-candidates/constrained-observation-theorems.md; docs/theory/advanced-directions/constrained-observation-results-report.md; tests/math/test_recoverability.py |
Promote as the stronger control-side threshold law and demote the older coordinate-only wording to a corollary. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-044 |
Boundary-compatible finite-mode Hodge projection |
On a bounded-domain family built from boundary-compatible divergence-free stream modes and Dirichlet gradient modes, the orthogonal projector onto the protected span is an exact bounded-domain correction operator. |
PROVED ON SUPPORTED FAMILY |
integration-by-parts derivation plus independent discrete projector-construction checks and tests |
Medium |
docs/theorem-candidates/bounded-domain-hodge-theorems.md; docs/theorem-candidates/cfd-projection-results.md; tests/math/test_cfd_projection.py; tests/examples/test_generated_artifact_consistency.py |
Promote as a restricted but real partial solution to the bounded-domain exact-correction problem. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-045 |
Restricted-linear minimal augmentation theorem |
For a restricted linear family x = F z with record O F z and protected variable L F z, the minimum number of unrestricted added linear measurements needed for exact recovery is δ(O, L; F) = rank([O F; L F]) - rank(O F). |
PROVED |
row-space derivation, random stress tests, and design-artifact consistency checks |
High |
docs/theorem-candidates/capacity-theorems.md; src/ocp/design.py; tests/math/test_design.py; tests/examples/test_design_examples_consistency.py |
Promote as the first finished category-specific capacity invariant beyond lower bounds alone. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-046 |
Restricted-linear exact-regime upper envelope |
If exact recovery holds on a restricted linear family and K satisfies K O F = L F, then κ_{M,p}(δ) ≤ |
|
K |
|
_2 δ for Euclidean record and protected metrics. |
PROVED |
direct linear derivation plus exact-case computational checks and generated recoverability artifacts |
Medium |
docs/theory/advanced-directions/pvrt-theory-program.md; docs/theorem-candidates/pvrt-theorem-spine.md; docs/theory/advanced-directions/constrained-observation-derivations.md; tests/math/test_recoverability.py; tests/examples/test_generated_artifact_consistency.py |
Promote as the strongest current κ upper bound, but keep it explicitly inside the exact restricted-linear branch. |
|
|
|
|
|
|
|
|
| OCP-047 |
Same-rank observation insufficiency |
In the restricted-linear branch, same-rank record families can have opposite exact-recovery verdicts; observation amount alone does not determine exact protected-variable recoverability. |
PROVED |
explicit construction plus dimension-stress tests |
Medium |
docs/theory/advanced-directions/pvrt-theory-program.md; docs/theorem-candidates/pvrt-theorem-spine.md; docs/theory/advanced-directions/pvrt-falsification-program.md; tests/math/test_recoverability.py |
Promote as the clean falsification of rank-only or amount-only recoverability language. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-048 |
Detectable-only through target coarsening |
If q = φ ∘ p, exact recoverability of p implies exact recoverability of q, while the converse can fail even on finite or restricted-linear families; exact recovery of such a nonconstant coarsening while p fails is the branch detectable-only regime. |
PROVED |
factorization argument plus finite and restricted-linear witnesses |
Medium |
docs/fiber-based-recoverability-and-impossibility/fiber-formalism-core.md; docs/fiber-based-recoverability-and-impossibility/fibers-and-detectability.md; src/ocp/fiber_limits.py; tests/math/test_unified_limits.py |
Keep as the fiber-based branch’s clean target-hierarchy theorem and use it carefully when translating detect-vs-correct language across fields. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-049 |
No rank-only exact classifier theorem |
For every n > r ≥ 1 and every r ≤ k < n, there exist restricted finite-dimensional linear recoverability problems with the same ambient dimension n, protected rank r, and observation rank k but opposite exactness verdicts, so no classifier depending only on (n, rank(LF), rank(OF)) can decide exact recoverability on all such families. |
PROVED |
explicit witness construction, exhaustive small-dimension coordinate enumeration, and generated artifacts |
High |
docs/fiber-based-recoverability-and-impossibility/restricted-linear-fiber-theory.md; docs/fiber-based-recoverability-and-impossibility/fibers-and-impossibility.md; src/ocp/fiber_limits.py; tests/math/test_unified_limits.py; data/generated/unified-recoverability/unified_recoverability_summary.json |
Promote as the fiber-based branch’s strongest surviving negative theorem and as the cleanest statement of where amount-only unification fails. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-050 |
No fixed-library budget-only exact classifier theorem |
For every n > r ≥ 1 and every r ≤ k < n, there exists a common coordinate candidate library with unit measurement costs and two selections of the same size k and same total cost k that have opposite exact-recovery verdicts, so fixed-library budget/count alone cannot decide exact recoverability on all restricted finite-dimensional linear families. |
PROVED |
explicit fixed-library construction, exhaustive subset enumeration, and generated artifacts |
High |
docs/fiber-based-recoverability-and-impossibility/restricted-linear-fiber-theory.md; docs/fiber-based-recoverability-and-impossibility/fibers-and-impossibility.md; src/ocp/fiber_limits.py; tests/math/test_unified_limits.py; data/generated/unified-recoverability/candidate_library_budget_witnesses.csv |
Promote as the stronger fixed-library version of the anti-universal theorem and use it against sensor-count/budget-only overclaims. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-051 |
Noisy weaker-versus-stronger separation theorem |
On a restricted linear family x = F z, if a weaker target W F z is exactly recoverable by K O F = W F while a stronger target S F z has positive collision gap Γ on the same bounded family, then bounded record noise |
|
e |
|
≤ η yields a weak-target error upper bound |
|
K |
|
_2 η while every decoder for the stronger target still has worst-case error at least Γ/2; in particular the weak upper bound stays strictly below the stronger impossibility floor for η < Γ/(2 |
|
K |
|
_2). |
PROVED |
restricted-linear derivation plus brute-force noise-grid cross-checks and generated artifacts |
High |
docs/fiber-based-recoverability-and-impossibility/fibers-and-weaker-vs-stronger-targets.md; docs/fiber-based-recoverability-and-impossibility/restricted-linear-fiber-theory.md; src/ocp/fiber_limits.py; tests/math/test_unified_limits.py; data/generated/unified-recoverability/noisy_restricted_linear_hierarchy.csv |
Promote as the branch’s strongest current noisy target-hierarchy theorem and use it to separate stable weak recovery from strong-target impossibility. |
| OCP-052 |
Restricted-linear family-enlargement false-positive theorem |
Let F_s and F_l be restricted-linear admissible family bases with span(F_s) contained in span(F_l). If exact recovery holds on the smaller family but ker(O F_l) is not contained in ker(L F_l), then exact recovery fails on the enlarged family; moreover the enlarged-family collision gap Γ_l yields the lower bound Γ_l/2 for every decoder on the enlarged family, including any decoder exact on the smaller family. |
PROVED |
fiber-factorization argument plus collision-gap lower bound, explicit witness construction, generated artifacts, and branch tests |
High |
docs/fiber-based-recoverability-and-impossibility/theorem-candidates.md; docs/fiber-based-recoverability-and-impossibility/false-positive-risk-report.md; docs/fiber-based-recoverability-and-impossibility/restricted-linear-fiber-theory.md; src/ocp/fiber_limits.py; tests/math/test_unified_limits.py; data/generated/unified-recoverability/family_enlargement_false_positive.csv |
Promote as the branch’s cleanest current admissible-family-enlargement false-positive certificate, with family scope kept explicit. |
|
|
|
|
|
|
|
|
|
|
|
|
| OCP-053 |
Canonical model-mismatch instability theorem |
On the canonical restricted-linear family F_beta = span{e1, e2 + beta e3} with record M(x) = (x1, x2) and target p(x) = x3, each fixed beta yields exact target identifiability, but the decoder exact on F_beta0 incurs worst-case exact-data target error |
beta - beta0 |
/ sqrt(1 + beta^2) on the true family F_beta over the unit coefficient box. Thus exact identifiability of the true family does not imply robustness of a mismatched inverse map. |
PROVED |
closed-form derivation plus brute-force equality checks and generated artifacts |
High |
docs/fiber-based-recoverability-and-impossibility/theorem-candidates.md; docs/fiber-based-recoverability-and-impossibility/model-mismatch-stress-report.md; docs/fiber-based-recoverability-and-impossibility/final-inverse-observability-pass-report.md; src/ocp/fiber_limits.py; tests/math/test_unified_limits.py; data/generated/unified-recoverability/canonical_model_mismatch.csv |
Promote as the branch’s cleanest current exact model-mismatch theorem, with canonical family scope kept explicit. |
|
|
|
|
|
|
|
|
|
|