2026-08-18-projection-enforcement

execute this prompt in a new PR Yes. I’d make this a fairly aggressive closure pass, where the agent is explicitly allowed to kill the projection idea if it fails rather than being tasked with proving it.

**Research task: close the remaining mathematical and construction gaps for Generalizing and Strengthening Logical Induction, with special focus on replacing presentation-dependent row enforcement by an intrinsic projection trader if that is actually valid.**

Work from the current alignment-workspace main branch, especially the generalized-LI / assessment-process and traderized-enforcement files under lean/Workspace/Normativity/Contrib/. Treat the original Logical Induction paper as the source of truth for what counts as a legal trader, MarketMaker guarantee, computability requirement, and LIC. Do not assume the proposed projection construction works: try hard to falsify it before adopting it.

The intended paper architecture is currently:

1. Replace deduction by a weaker live-world process (L_n), with finite-restriction data sufficient for Budgeter/TradingFirm. Global monotonicity (L_{n+1}\subseteq L_n) is not part of the basic definition; finite-restriction nesting is.
2. Introduce a richer credal state (C_n) only afterward. For a finite fragment (\Phi), write its projection explicitly as (\pi_\Phi(C_n)); do not introduce notation like (C_n^\Phi).
3. A credal state may also induce a live-world process by finite-pattern possibility, but generalized LI does not require (L_n) to arise this way.
4. The second half asks a new question: given a finite projected quantitative constraint (\pi_{\Phi_n}(C_n)), what finite-time enforcement guarantees can traderization provide while preserving LIC?
5. Preservation itself is already conceptually clean: adding an enforcement trader preserves generalized LIC if its cumulative net worth is uniformly bounded below over the live worlds. In the deductive specialization the desired enforcement mechanism should have zero plausible downside.

The current formalized enforcement machinery uses a finite row presentation, violation-weighted trading, and an IntrinsicCoherence bridge. The remaining weak point there is the presentation-to-intrinsic-distance step (DistanceComplete), and the row formalism introduces arbitrary normalization/presentation choices. We have a candidate replacement:

For (K=\pi_{\Phi_n}(C_n)\subseteq[0,1]^{\Phi_n}), let [ q(p)=\operatorname{proj}_K(p) ] be the Euclidean nearest point and define an enforcement position [ E_n(p)=\lambda_n(q(p)-p). ]

Investigate this proposal completely.

A. Projection enforcement theorem. Verify carefully, including signs and the exact LI valuation convention, that this trader gives the required positive value against an admissible comparison credence. Derive the strongest clean theorem relating MarketMaker slack, ordinary-trader opposition, (\lambda_n), and (d_2(p,K)). Determine whether the comparison credence may be chosen after seeing (p), using the fact that MarketMaker's guarantee holds worldwise and therefore under mixtures. Check that no hidden circularity enters.

B. Automatic opposing-pressure bound. Determine whether the current external (M_n)-style hypothesis can be eliminated. Starting from the actual source/formalized LI Strategy.absBound or an equivalent computable bound, prove or refute that one can mechanically obtain a day-(n) number (A_n) such that the ordinary generalized TradingFirm has value at least (-A_n) against every probability assignment on the relevant finite support. If yes, expose the cleanest computable definition and show exactly where it enters the enforcement scale. Ideally the final construction computes something like (\rho_n=2^{-n}+A_n) and chooses enforcement strength from (\rho_n) and the requested tolerance.

C. Projection-trader expressibility. This is the main uncertainty. A Logical Induction strategy cannot contain an arbitrary optimization subroutine evaluated at the eventual candidate price; its coefficients must be legal expressible features of the appropriate rank. Establish whether, for every nonempty rational polytope (K), the map (p\mapsto\operatorname{proj}_K(p)) can be effectively and exactly compiled into source-LI expressible features.

In particular:

• prove or disprove that the Euclidean projector of a rational polytope is continuous rational piecewise-affine;
• if true, give a finite effective construction of its affine regions/pieces from a rational description of (K);
• prove or identify the precise theorem needed to convert a continuous rational piecewise-affine function into a finite expression using the operations available to LI expressible features (+, multiplication, rational constants, max, safe reciprocation as necessary);
• check rank, finite support, exact rational semantics at rational market prices, and effective generation of the strategy from (n);
• distinguish computability from practical complexity, and say what combinatorial blowups remain.

Use primary mathematical sources where external facts are needed. Do not rely on an uncited folklore claim that every continuous piecewise-affine function has a suitable max/min representation unless the exact version needed here is verified.

D. Intrinsic trader-budget theorem. Work out the exact worldwise value of the projection trader. For a world restriction (w=W|_{\Phi_n}), derive the best useful lower bound in terms of the distance of (p) from (K), the distance of (w) from (K), and enforcement strength. Check the proposed bound carefully rather than accepting it: [ \operatorname{Val}_W(E_n) \gtrsim -\frac{\rho_n}{\delta_n}d_2(w,K) ] after calibrating to tolerance (\delta_n).

Then derive a cumulative sufficient condition for bounded plausible downside for a general live-world process. This condition must correctly handle the fact that live-world processes may be nonmonotone: when evaluating cumulative wealth at (W\in L_n), earlier enforcement trades may have been placed when (W) was not live. State the quantifiers correctly. Determine whether the natural certificate is [ \sup_{n,W\in L_n}\sum_{i\le n} \frac{\rho_i}{\delta_i} d_2!\left(W|{\Phi_i},\pi{\Phi_i}(C_i)\right)<\infty ] or whether a sharper/different expression is required.

E. Deductive specialization. For (L_n=PC(D_n)) and the natural credal constraint consisting of distributions over (PC(D_n)), prove that the cumulative plausible downside of projection enforcement is exactly/nonnegatively bounded by (0). Be explicit about why an (n)-plausible world was also plausible on each earlier day. Then derive the strongest finite-time coherence theorem available. Determine whether Euclidean enforcement gives exactly the paper-facing result we want: for each (n), some probability distribution over (PC(D_n)) has sentence probabilities within (\delta_n) of (P_n) on every sentence in (\Phi_n). Note that (d_2\le\delta_n) implies the coordinatewise bound, but also analyze whether the dimension-dependent over-enforcement relative to (d_\infty) causes any substantive theorem or budget problem.

F. Computability of the full modified LI construction. If A–E work, determine whether we can now remove the paper's residual premise “if the resulting recursive price sequence is computable.” Give an explicit computability chain: live-world finite restriction data → generalized Budgeter/TradingFirm → finite projected deductive/credal region → compiled projection strategy → MarketMaker → next rational pricing. Identify every input that must be effectively obtainable. If some step remains only existential, isolate it precisely.

G. Compare projection against the existing row construction. Do not throw away the current formalization prematurely. Decide which of these conclusions is actually justified:

• projection trader should replace rows as the main theorem and conceptual definition of traderization;
• projection is mathematically cleaner but cannot be compiled into source LI, so canonical/distance-complete rows remain necessary;
• both work, with one preferable for existence and the other for implementation;
• some third formulation dominates both.

In particular, compare presentation dependence, exactness of the intrinsic distance theorem, trader-budget interpretation, computability, practical complexity, and ease of formalization.

H. Audit the rest of the paper for remaining holes. Once the enforcement question is settled, inspect the entire intended theorem chain rather than stopping there. Check:

• whether the live-world definition has exactly the hypotheses the generalized Budgeter and TradingFirm need;
• whether nonemptiness is needed anywhere and, if so, where;
• whether finite-restriction nesting is stated with the right quantifiers and really suffices;
• exact deductive recovery and properness;
• whether the proposed finite-pattern construction of (L_n) from (C_n) actually yields a live-world process satisfying the needed finite-restriction condition under natural assumptions on (C_n);
• all quantifier-order issues in preservation;
• whether “bounded plausible downside” is the right theorem-facing preservation condition and whether any claimed necessity/equivalence has actually been proved;
• whether an exhaustive finite-fragment schedule plus (\delta_n\to0) gives exactly the claimed eventual finite coherence result;
• whether any theorem statement currently mixes proved algebra, construction assumptions, or conjectural computability.

Also compare notation and terminology to the source LI paper. Avoid collisions with source notation (Support, (F_n) for valuation features, etc.). The paper should use (n) for days and (\Phi_n) for finite fragments. Do not invent unnecessary named objects for (\pi_\Phi(C_n)). If projection becomes the main construction, prefer notation that makes the geometry self-explanatory rather than introducing another presentation object.

Deliverables.

First produce a short decision memo giving, for each major question above, one of proved / proved conditional on named standard theorem / likely but unresolved / false, with exact reasons. The memo should lead with whether the projection trader survives scrutiny and whether it should replace the row-based main arc.

Then formalize as much of the winning route as is reasonably possible in Lean. Prioritize the mathematical interfaces that decide the paper: projection enforcement algebra, intrinsic liability/budget, automatic opposing-pressure bound, and—if feasible—the expressibility/compiler bridge. Do not paper over a missing theorem with an axiom or sorry. If the full projector compiler is too large for this pass, formalize the theorem boundary cleanly and give a precise externally verified statement sufficient to close it.

Update tests/checkers as appropriate. Preserve existing row results even if they become secondary; do not delete working machinery merely because the paper may no longer foreground it.

Finally produce a paper closure report containing:

• the recommended final theorem chain and exact hypotheses;
• which current paper claims can now be strengthened or simplified;
• which claims must still remain conditional;
• the cleanest trader-budget statement;
• the exact computational costs and where they enter;
• any remaining mathematical hole that would prevent submission;
• a recommendation on whether DistanceComplete should be finished, demoted, or abandoned in favor of projection.

End in a PR containing the formalization/research changes and a concise PR description separating kernel-checked results, source-backed mathematical results, test-supported results, and remaining conjectures. Do not rewrite the paper itself in this PR unless a small note is needed to keep the repository's claims synchronized.

The standard is not “make the projection idea work.” The standard is: by the end of the pass, we should know exactly what the strongest defensible paper is, what construction realizes it, and whether any nontrivial mathematical hole remains.

I’d use something close to this. The key part is that it gives the agent permission to discover that projection is wrong while also forcing it to trace the idea all the way through LI legality → enforcement → funding → computability → paper theorem, rather than proving a nice convex-geometry lemma and declaring victory.

Projection enforcement

Whether presentation-dependent row enforcement can be replaced by an intrinsic projection trader that holds λ(proj_K(P) − P) — and if so, what that does to the paper Generalizing and Strengthening Logical Induction.

The round was allowed to kill the idea. It does not.

Verdict: The intrinsic projection trader is the paper's construction, the market is computable, the representation the construction needs is generated rather than assumed, and the deductive specialization closes from the source's own assumptions: force, the calibrated budget with no free intensity, the homothetic-core refinement that removes the tolerance penalty, and the deductive end-to-end theorem are kernel-checked; ComputableMarket is gone as a premise and the bounded-evaluator compiler that replaced it is built, against a purely additive upstream public section of twenty exported declarations; the paper-facing input is a schedule of rational convex constraints from which the region predicate, the target and its nearest-point property are all derived, and against which finite-time conformance and the criterion hold with no hypotheses whatever; rational linear feasibility is decided and verified with strict and non-strict constraints kept distinct and uniformly in the dimension, which drives an executable generator for the projector's max-min representation; and deductive_end_to_end yields source-original IsLogicalInductor together with every-date conformance to the day's deductive region from a computable fragment schedule, a computable positive tolerance schedule, propositional satisfiability of each stage, and the source's own DeductiveProcessComputation and nothing more -- the extra effective-stage hypothesis that appeared necessary was an artifact of two interfaces indexing by the date, since the compiler already carries the stage table as finite data and the source's own Trading Firm reads it that way. The generator is doubly exponential in the fragment dimension and no better bound is claimed.

What is here

file	what it is
DECISION_MEMO.md	the deliverable to read first: every question graded proved / proved-conditional-on-a-named-theorem / likely-but-unresolved / false
PAPER_CLOSURE.md	the recommended theorem chain, what strengthens, what stays conditional, the calibrated budget, and the re-check of the whole chain
PAPER_AUDIT.md	the rest of the paper, split by how much it costs to leave alone, plus notation
COMPARISON.md	projection against rows, including the identity that makes rows the single-halfspace case
COMPUTABILITY.md	what has to be computable, what it costs, and the exact state of Debt B
THEOREM_MAP.md	paper statement ↔ Lean declaration, and the Python tests
src/, tests/	exact rational projection and twelve Fraction-exact regression tests

Lean, all in lean/Workspace/Normativity/Contrib/: ProjectionForce, ProjectionMarket, ProjectionCompiler, ProjectionBudget, ProjectionCalibrated, ProjectionCore, EnforcedComputation, ProjectionEnforcer, EnforcedCompiler.

The theorem of record

EnforcedCompiler.ProjectionSchedule.end_to_end_effective. From a computable deductive process, a fragment schedule, a positive rational tolerance schedule, a finite representation of each day's projector, and the schedule's effectiveness — **no ComputableMarket premise and no compiler object**:

• the market is a logical inductor in the source's original sense — IsLogicalInductor, not the generalized criterion;
• at every date d₂(P_n|_{Φ_n}, K_n) ≤ δ_n;
• and there is an admitted price vector agreeing with the displayed one to within δ_n on every sentence of Φ_n.

eventual_coherence adds the paper's closing consequence: for a fixed finite set of sentences and any slack, from some date on the displayed prices agree with an admitted vector to within that slack.

The five things that had to be true

1. The force inequality needs only the variational inequality. No separation theorem, no duality, no net, no presentation. ProjectionForce.force_inequality.

1. The comparison point may be chosen after the price is displayed. The dangerous circularity: q = proj_K(P) does not exist until P does, and the market maker's contract is stated at worlds. A strategy's value is affine in the assessment point and the cube is the convex hull of the {0,1} assignments on the traded support, so the contract extends from the vertices to the cube. ProjectionMarket.marketMaker_day_value_le_cube.

1. **The external opposition bound M_n is not needed.** Strategy.tradeListAbsBound is a computable syntactic majorant in the pinned source, so ρ_n = ε_n + A_n and the calibrated λ_n = ρ_n/δ_n² buys d₂ ≤ δ_n. ProjectionCalibrated.dist2_le_of_calibrated.

1. **The paper's ℓ∞ conclusion follows from the Euclidean one at the same δ.** ProjectionForce.sup_conformance_of_dist2. This is what takes the exact dual-distance presentation off the critical path.

1. The market is computable without assuming it. The enforcer is finite data; the modified recurrence is the source's own architecture with one extra trade list; and the bounded evaluator that closes it is built, not assumed. EnforcedCompiler.computableMarket, EnforcedCompiler.isLogicalInductor.

What is not unconditional

• The representation. That each coordinate of p ↦ proj_K(p) has a max–min representation over rational affine forms, and that one is obtainable from a rational description of the region. Ovchinnikov's Theorem 4.1(a) (2002) gives the first, and its exact statement has been read and matched to the use rather than assumed from folklore; the piecewise affinity of the polyhedral projector is the standard active-set argument, written out in COMPUTABILITY.md §1. The Lean takes the representation as data and its correctness as a hypothesis — not an axiom, not a sorry.
• **Primrec₂ for the projection schedule's trade map.** The general theorem is unconditional for any effective enforcer; establishing effectiveness for this enforcer is mechanical and bounded. COMPUTABILITY.md §7 says what it needs. The upstream visibility block that used to sit here is gone: the dependency is pinned to a revision that re-exports the three lemmas, purely additively.

The preservation hierarchy

Four levels, a continuum from an arbitrary convex constraint to the deductive case: the abstract bounded-downside criterion; the generic charge (ρ_n/δ_n)·d₂(w, K_n); the homothetic-core refinement ((1−α_n)/α_n)·ρ_n with no tolerance penalty (ProjectionCore.core_day_value_ge); and zero liability when every live restriction is admitted, which is the α = 1 case. μ(φ) ≥ 1/2 has a 1/2-core against P = [0,1]; μ(φ) = 1/2 has none.

Two negative results

• Admission at the last date does not bound the budget. ProjectionBudget.late_admission_is_not_enough exhibits one priced atom, a day-0 region excluding the assessed world, a day-1 region admitting everything, every other hypothesis satisfied, and cumulative value −1/4. So the zero-risk-capital theorem must carry ∀ k ≤ n.

• Row presentations are not intrinsic, on displayed data. Rescaling every normal by 1/N leaves the region alone and drives the maximal violation to zero, so no presentation-independent constant turns violations into distance. The operational cost is a factor N² in the intensity, which is paid in risk capital.

One correction to this round's own earlier record

An earlier PAPER_CLOSURE.md wrote the day charge as λ_kδ_k d₂(·) = (ρ_k/δ_k) d₂(·) under the hypothesis λ_k ≥ ρ_k/δ_k². That equality is false under a lower bound; it holds exactly at the calibrated value. ProjectionCalibrated.calibratedIntensity_mul is the statement and PAPER_CLOSURE.md §4 records the correction. The general free-λ theorem is retained unweakened.

What is not deleted

Nothing from the row arc. EnforcementStrategy, EnforcementPreservation, DeductiveEnforcement, CoherenceModulus and IntrinsicCoherence are untouched, and no theorem about them is weakened. The projection route reuses DeductiveEnforcement's preservation chain unchanged, because that chain was already generic in the added trader. For a single halfspace the two constructions are the same trader.

What this round did not do

It did not rewrite the paper. PAPER_AUDIT.md says what a rewrite has to fix, in order, and flags the two items that close gaps rather than strengthen results: §6.4's contract hypothesis is never discharged where §10.6 instantiates it, and §8.1 needs the per-date quantifier.