Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 46 additions & 0 deletions research/characteristic-gaussian-provider/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
# Constructive Gaussian-provider improvements

Dugongue, with substantial OpenAI Codex assistance from four workers. Pure informal mathematics: no numerical computation, solver, Lean check or external search was used. Local DAG, linked Lean-tree sources and retained provider notes supplied the precedents.

**Main result:** the actual whole-K/E coded negative terminal can be closed to its full independent Gaussian rank with one rank-2 query, replacing the previous two rank-1 repair queries. The construction preserves absolute phase, works at every positive lifted width, gives explicit ordinary XOR-coordinate normalizers, and retains independent inputs, owned-storage cleanup and reciprocal orientations.

**κ status:** no higher complete multiplication κ is proved. The new full-rank repair strictly reduces its own concave tariff, but the supplied complete whole-K/E invoice still does not yield a profitable supplier. The older rank-dropping repair also remains better under the isolated concave-moment comparison. The notes state these distinctions explicitly; none of the mathematical profiles below is advertised as a new selected record.

## Five notes and concrete results

1. [decoder.md](decoder.md), D1–D7: characteristic-translation symmetry exposes a second commuting Gaussian direction. For the actual terminal Q₀^(-1) P D, the sequence Qχ Q₀ followed by P^(-1) returns a full Gaussian in an explicit new binary basis. The two first factors fuse into one rank-2 child. The note proves phase, inverse/transpose, finite-precision and complete-invoice statements.
2. [current-provider.md](current-provider.md), Theorems 1–9: an exact rank-selective autonomy conversion for the actual eight-mode coupled provider; same-profile inverse/dual constructions; a complete full-rank promotion of all 632 independent inputs; and a general mixed-triangular central-promotion theorem. The physical W/Z intertwiners, rather than an unjustified logical-coordinate conjugation, drive the proofs.
3. [typed-provider.md](typed-provider.md), T1–T7: exact B/C fusion; ordinary role-subspace gauges with a defect-rank query tariff; reciprocal-dual compatibility; and sector-multiplexed queries. A complete two-field example shares one Gaussian query across complementary sectors where separately factored implementations use two. A profitable selected-provider instance is not asserted.
4. [whole-k.md](whole-k.md), K1–K8: a faithful embedding of a degenerate product-cube support into a smaller even binary ambient space. At three factors the native primitive is rebuilt in dimension 18, with four actual native child ranks 8,9,8,9 instead of 8,9,15,16. Physical owner codes and modal queries are rebuilt consistently, including changed target dimensions. Its two-rank-1 complete repair is improved by the companion decoder note.
5. This README supplies the assembly map, scope and source credit. The other four notes contain 31 numbered constructive lemmas/theorems/corollaries in total, with informal proofs, plus explicit comparisons and source-specific qualifications. This count describes this release only; it is not an inherited atlas count.

The quantities in the notes are symbolic mathematical profiles and exact algebraic consequences. They were derived by proof, without running numerical searches or executable mathematics. Publication helpers outside this directory only transport frozen document bytes.

## Assembly: what can already be used

The full-rank decoder applies immediately to either the original ambient-25 whole-K/E code, retaining its own rank-73 targets, or the newly reconstructed ambient-18 code, whose three fresh stages have rank-52 targets. It replaces only the terminal repair. Replacing the old local bill by the smaller one while retaining rank-73 targets is invalid.

For the compressed case, with v = 112³ and h = 20480, the complete closed provider is

independent targets: 2v H₅₂,
Gaussian requests: 3v(2 H₈ + 2 H₉) + 3h H₁₈ + v H₂.

Compared with the previous full-rank repair, its target-minus-paid moment improves by v(2 − 2^t) for every 0 < t < 1. This exact improvement is insufficient to change κ, as D7 proves from the complete invoice. Ordinary code costs, effective coefficient descriptions and field-volume precision guards remain charged. No complexity theorem is inferred from a query profile alone.

The current eight-mode provider has a different interface. Its complete autonomous promotion returns productive profile {4:28, 7:7, 8:47, 9:550} at paid profile {1:2425, 2:412, 3:510, 4:127, 5:40}. This is a proved all-input completion, not a profitable supplier asserted from nominal helper credit. Its selected-mode offers preserve the remaining coupled outputs instead of silently discarding them.

The sector-multiplexing theorem is a complete query-sharing algorithm for its stated operators. It can be used whenever ordinary involution-sector coefficient blocks actually occur. Scalar-only boundaries with identical sector coefficients do not automatically gain from it. No such saving is subtracted from the current provider's bill in this release.

## Exact scope and remaining work

The release supplies positive sufficient constructions with full informal operator proofs. It does not formalize them, emit a native implementation, establish new literature priority, or certify a new best numerical κ. The principal mathematical assembly task remains a complete profitable provider or consumer combining one of these constructions with actual independent output credit. Uniform compilation must then account for all ordinary work, coefficient access, word widths, storage and error, using the exact interface that was proved.

Only retained local sources were available for comparison. The inspected canonical snapshot is `5e0052ca0aa3036a3afa8b0438927377c8d97d53`; no claim is made to have refreshed later upstream submissions during this no-web session. This release changes no selected frontier.

## Predecessor credit and proof-tree connections

The current-provider lineage includes Dillon Amburgey's PR5402, Chris R/Clear1nsight's PR5407 and PR5413 audit/completion, Ali Romman's PR5377/PR5383 relation work, Cinna Davis's PR4694/PR4698 code work, and Cao Yifan's native word. The reconstructed whole-K/E lineage includes THU New Media Research Center/PR5464, Ali Romman/PR5439 and the retained native/Clifford sources. The typed-interface lineage includes DaysSky's quotient route, Cinna Davis and the controller sources, Nick Petalas, Ryanson Jonathan and Dugongue. Credit also Jacob Alan Sussman, zxv, the scalar/compiler/analytic lineage, Harvey and van der Hoeven, and the individually cited source authors. Each note gives its relevant source-relative documents; these credits do not assert that every predecessor endorsed the new arguments.

The linked proof tree's `Mathproof/SymplecticTI.lean`, `Mathproof/LibraryBridges/Claude/TISpTransporterFibers.lean` and `Mathproof/SymplecticTITOCIBalancedCoevaluation20260901.lean` informed explicit transporter, independent-support and invariant-subspace bookkeeping. No tensor-isomorphism algorithm is invoked as a Gaussian oracle. Classical binary-form, rank-factorization, Fourier-sector, triangular-elimination and elementary Gaussian identities remain classical; the contributions here are their stated concrete provider constructions and complete endpoint accounting.

Recommended review order: decoder D1–D3 and D6–D7; whole-K K1–K6; current-provider Theorems 1 and 8–9; typed-provider T3 and T6–T7. Every κ-related assertion should be read together with its full independent target and paid profiles.
Loading