compiler.deductive-end-to-end

Bridge card

A conjunct of the informal claim traderized-finite-date-conformance: A constraint on prices compiles to a legal trading strategy inside the market recursion, giving per-date conformance within a schedule while preserving the logical induction criterion.

Declaration Workspace.Normativity.Contrib.DeductiveEffective.deductive_end_to_end in lean/Workspace/Normativity/Contrib/DeductiveEffective.lean (record compiler.deductive-end-to-end.record)

Registry compiler.deductive-end-to-end: class lean-proved, status active, review ci-only, origin round 2026-08-18-projection-enforcement; bears on item 48

Hypotheses, read:

• compiler.deductive-end-to-end.h-fragment-schedule definitional: The fragment schedule assigns each date a duplicate-free list of sentences and is primitive recursive.
  The binders `coords`, `nodup` and `hcoords`: the schedule object's own data and its computability, read as one hypothesis. Definitional: it says what a fragment schedule is, and asks nothing of the deductive process.
• compiler.deductive-end-to-end.h-tolerance-schedule definitional: The tolerance schedule assigns each date a strictly positive rational and is primitive recursive.
  The binders `tol`, `tol_pos` and `htol`, read as one hypothesis. Definitional: the schedule's own data; any computable positive schedule serves.
• compiler.deductive-end-to-end.h-process-certificate definitional: The deductive process carries the pinned source's own computability certificate: a program that eventually emits each stage.
  The binder `process : DeductiveProcessComputation DP`. Definitional: the source's definition of a deductive process (a computably enumerable stage sequence), the hypothesis the source's own theorem carries, and no restriction added by this declaration; the file's header says no hypothesis about the process beyond the source's own is needed.
• compiler.deductive-end-to-end.h-stages-satisfiable open: Every stage of the deductive process is propositionally satisfiable: some propositionally consistent world agrees with the stage.
  The binder `hsat`. Open: a consistency assumption on the process that the declaration consumes and does not derive; the source's deductive processes are consistent by stipulation, and a reader granting the claim for a given process must grant this of it. It does not restate the conclusion.

Completeness (compiler.deductive-end-to-end.complete): No premise beyond the signature's binders enters the declaration; the kernel checks it as stated. The result is the record, the four hypothesis leaves filed by reading (the fragment schedule, the tolerance schedule, the pinned source's computability certificate on the process, and the satisfiability of every stage), the bridge and this leaf; the premise list is the signature's, grouped as a reader states it.

What remains (traderized-finite-date-conformance.improvable)

The compiled per-date conformance, in which a constraint on prices compiles to a legal trading strategy that conforms within a schedule while preserving the criterion, can be improved until it reflects a logical inductor whose prices answer a normative seed's constraints under a finite liability account well.

• item-129: The compiled enforcer's per-day gap bets are bounded below by a schedule while the criterion is preserved, so that the conformance the compiler gives is a trust bound the deference line can read. — this is item 129
• route-conformance-credal-constraint: Normative statics produce a credal constraint on prices rather than only a price demand, so that what the compiler enforces is the seed's own constraint. — item 39
• route-conformance-efficient-rows: An efficiently presentable sufficient row family for coherence replaces the doubly exponential generator the declaration's construction uses. — item 42
• route-conformance-exact-and-safe: A compiler that is both exact and conformance-preserving exists, or a proof says there is none, so that conformance within a schedule is not bought by inexactness. — item 43
• traderized-finite-date-conformance.residual (residual): A refinement of the compiled conformance that none of the other routes describes reflects a logical inductor whose prices answer a normative seed's constraints under a finite liability account.