diff --git a/research/productive-helper-dimension-floor/.gitattributes b/research/productive-helper-dimension-floor/.gitattributes new file mode 100644 index 0000000000..44a23d1fe3 --- /dev/null +++ b/research/productive-helper-dimension-floor/.gitattributes @@ -0,0 +1,2 @@ +* text eol=lf +*.gz binary diff --git a/research/productive-helper-dimension-floor/PATHS.json.gz b/research/productive-helper-dimension-floor/PATHS.json.gz new file mode 100644 index 0000000000..cb5c70f1c6 Binary files /dev/null and b/research/productive-helper-dimension-floor/PATHS.json.gz differ diff --git a/research/productive-helper-dimension-floor/PROOF.md b/research/productive-helper-dimension-floor/PROOF.md new file mode 100644 index 0000000000..ad42790119 --- /dev/null +++ b/research/productive-helper-dimension-floor/PROOF.md @@ -0,0 +1,117 @@ +# Fixed projection dimensions: arbitrary Lagrangian chart obstruction + +This source-specific theorem concerns the unchanged round-three word in each orientation, with all +chronological paid incidences retained and the eight owned center costs fixed. +It does not fix the subspace direction or its quadratic form. At each node it +fixes only the dimension of the chart's projection onto the first (x) half of +the binary symplectic coordinates, equal to the original frame dimension. + +The source is `research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz`. +The canonical compact JSON payload SHA-256 is +`cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd`. +The separately reconstructed program hashes are +`03e406a5672ada3e1762011d667c79ec04a55d7d1163a9423d0005720234d2ca` +(forward) and +`a4ff7b7ca8f23c858f8e6f1044bc6abf92168ab17abd2aa420ad384f58a519d3` +(backward), under the same sorted-key compact JSON convention. + +Write V = F_2^n x F_2^n with its usual symplectic form and let Z = 0 x F_2^n. +For a physical frame F, use the **inverse-image** chart L(F)=F^-1(Z), an +n-dimensional Lagrangian. A paid physical transition is F_next F_prev^-1; +its Fourier rank is + + d(L(F_prev),L(F_next))=n-dim(L(F_prev) intersect L(F_next)). + +Forward images F(Z) cannot be substituted for these inverse images for a +general frame. This convention and the exact symmetric-phase chart grammar +are documented in `research/native-quotient-interface/PHASE-FORM-GRAMMAR.md`; +the canonical specialization is in +`research/complex-frame-distance-seed80/PROOF.md`. Let k(L)=dim pi_x(L). +Signs, affine +translations and overall phases do not change this rank; granting them +freely only enlarges the geometric relaxation. No physical compiler or +endpoint phase admission follows from a rank obstruction. + +## Projection lower bound and rigid zero entrances + +Rank-nullity gives dim(L intersect Z)=n-k(L), hence d(L,Z)=k(L). The +Grassmann/subspace distance d on equal-dimensional subspaces is a metric. +Its reverse triangle inequality therefore gives + + d(L,M) >= |d(L,Z)-d(M,Z)| = |k(L)-k(M)|. + +For completeness, triangle inequality follows from +dim(L intersect N) >= dim(L intersect M)+dim(M intersect N)-n: the two +intersections are subspaces of the n-dimensional M, and their intersection +lies inside L intersect N. This proves the needed metric statement without +any isotropy assumption beyond the common dimension. + +This metric is standard: Koetter and Kschischang, *Coding for Errors and +Erasures in Random Network Coding*, section 3.1, Lemma 1, proves the subspace +metric dim(A)+dim(B)-2dim(A intersect B). On equal n-dimensional spaces the +distance used here is half that metric. The source-specific path accounting, +not the metric identity, is the new application: + (v2, 25 March 2008). + +If k(L)=0, then L=Z. Consequently a helper with zero entrance projection has +rank k(M), regardless of its exit's quadratic form or projection direction. + +The original paid edges are nested canonical charts, so their original ranks +r are the nonnegative differences of the source frame dimensions. Arbitrary +new Lagrangians with the same per-node projection dimensions have paid ranks +r+delta with delta>=0. In contrast to the canonical theorem, delta need not +be even. Every original native rank is zero, so arbitrary changes of native +maps cannot decrease their cost. Owned costs are held fixed. + +## Incremental concavity pays each helper credit + +Let H be any nondecreasing concave function on all nonnegative reals, with H(0)=0. +For r_i,delta_i>=0 put R=sum r_i and D=sum delta_i. Diminishing increments +of a concave function imply, with s_i=sum_{j= H(R+s_i+delta_i)-H(R+s_i), + +because r_i<=R+s_i. Summing telescopes and proves + + sum_i [H(r_i+delta_i)-H(r_i)] >= H(R+D)-H(R). + +For a paid-only source-geodesic helper wire, R equals its original residual +rank. The metric triangle inequality bounds its new residual q by R+D. +Monotonicity of H then shows that the increase in the wire's paid tariffs is +at least H(q)-H(R), its entire additional helper credit. This remains true +if q= |k(L)-k(M)|` shows that every original nested paid edge +already has the smallest possible rank at its endpoint heights. Changing +charts at fixed heights cannot make any such edge cheaper. Source native +transitions have rank zero and cannot get cheaper either. + +Of 408 helpers, 358 have height-zero entrances, whose charts are necessarily +`Z`; their residual ranks remain fixed. Each of the other 50 has a paid-only +entry-to-exit wire whose source rank sum equals its original helper residual. +These paths share no charged edge occurrence. Every old-zero edge is retained. + +If a path's source ranks are `r_i` and their increases are `delta_i >= 0`, +concavity gives + +```text +sum_i [H(r_i+delta_i)-H(r_i)] + >= H(sum_i r_i + sum_i delta_i) - H(sum_i r_i). +``` + +The metric triangle inequality bounds the new helper residual by the new +path rank sum. Thus each path pays for its helper's entire additional credit; +edge-disjointness prevents reuse of that payment. All other costs are +nondecreasing. [PROOF.md](PROOF.md) gives the full argument for any +nondecreasing concave tariff on nonnegative reals with `H(0)=0`. + +## Reproduction + +Python 3.12, standard library only: + +```sh +python3 -B scripts/research_package.py --package research/productive-helper-dimension-floor --check-only +python3 -B scripts/research_package.py --package research/productive-helper-dimension-floor +python3 -I -O -B research/productive-helper-dimension-floor/verify.py +``` + +The direct replay prints `PASS_PRODUCTIVE_HELPER_DIMENSION_FLOOR`; the +registered runner also prints `PASS_REGISTERED_RESEARCH_PACKAGE`. + +The checker authenticates the compressed source and its complete JSON +payload, reconstructs both chronological graphs, validates every source +native rank and the full paid/helper invoices, and records all 50 paths per +orientation in the deterministic `PATHS.json.gz` receipt, bound by +[RESULT.json](RESULT.json). Each orientation has 1,016 selected +paid edge occurrences. All 448 source adapters touch only main roles. + +Eight corruption controls reject source changes, missing old-zero edges, +double-counted debt, and native transitions inserted into paid-only paths. +A separate finite calibration enumerates all Lagrangians in dimensions one +through three and checks the height/rank convention on 18,459 ordered pairs. +These checks remain active under `python -O`. The checker imports no +predecessor graph builder, compiler, optimizer or numerical library. + +Parent and independent agents checked the source paths and the argument +separately. This is not independent human or proof-kernel acceptance. No +new physical word is emitted, and no new phase, compiler, precision, supplier +or outer-theorem admission is asserted. + +## Scope, sources and credit + +The only live input is Cao Yifan's round-three word from +`research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz`, pinned in +[SOURCES.json](SOURCES.json) at canonical main +`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. This original-source theorem does +not depend on the compression or finite fusion certificate in +[PR #5301](https://github.com/CrocSwap/integer-mult-bounds/pull/5301). + +Each node may choose any Lagrangian chart of its original projection +dimension, including a different projection direction and quadratic form. +Compatible shared native maps may change. The proof even allows independent +native maps at different occurrences and independent chart choices between +orientations; actual physical constraints may narrow this relaxation. +Owned-center tariffs and helper contracts remain fixed. Changed projection +dimensions, owned costs, scalar/contact graphs, helper contracts and other +supplier mechanisms are outside the theorem. + +Related path-floor work includes Matarener's +[PR #5060](https://github.com/CrocSwap/integer-mult-bounds/pull/5060), Cinna +Davis's [PR #5136](https://github.com/CrocSwap/integer-mult-bounds/pull/5136) +and [PR #5140](https://github.com/CrocSwap/integer-mult-bounds/pull/5140), and +zxv's arbitrary-Clifford owned-tree extension in +[PR #5283](https://github.com/CrocSwap/integer-mult-bounds/pull/5283). +Those concern owned-center or other constrained path costs. The contribution +here is the source-specific 50-helper path census and complete-invoice +accounting at fixed heights. [PR #5144](https://github.com/CrocSwap/integer-mult-bounds/pull/5144) +provides distinct nonmonotone owned/shared-map context. The subspace metric +and concavity principles are standard; the proof credits the metric's +Koetter–Kschischang reference and the retained inverse-chart grammar. + +Overlap checks read the start/handoff/native discussion context and an initial +800 most-recently-updated PRs, followed by a 100-PR delta on 2026-10-23 ending +at 13:09 UTC. This is bounded coverage, not a census of unpublished work or +all open PRs. Canonical main was refreshed before this package. + +Credit Cao Yifan's #4610 source word, Cinna Davis's canonical/native and helper +accounting lineage, Dugongue's chart contract, zxv's supplier, and all retained +scalar/Clifford/compiler authors. Prepared by flyingviper with substantial +OpenAI Codex assistance and independent agents. Apache-2.0. + +## Open next questions + +Can a coordinated change of contact heights and native interfaces lower the +complete invoice? Start with a concrete source-derived dimension change and +its full signed paid/helper polynomial, then optimize the coupled native +interfaces while charging every old-zero edge. A favorable exact invoice +still needs one compatible shared map per operator and the applicable dual +native, phase, compiler and outer checks. [TASK.json](TASK.json) records this +scope change, first step and blockers. diff --git a/research/productive-helper-dimension-floor/RESULT.json b/research/productive-helper-dimension-floor/RESULT.json new file mode 100644 index 0000000000..b481b5e249 --- /dev/null +++ b/research/productive-helper-dimension-floor/RESULT.json @@ -0,0 +1,131 @@ +{ + "status": "PASS_FIXED_PROJECTION_HEIGHT_CLIFFORD_OBSTRUCTION", + "source_sha256": "cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd", + "directions": { + "forward": { + "program_sha256": "03e406a5672ada3e1762011d667c79ec04a55d7d1163a9423d0005720234d2ca", + "nodes": 19197, + "paid_edge_occurrences": 34398, + "native_edge_occurrences": 240, + "source_native_ranks_all_zero": true, + "source_main_adapter_occurrences": 448, + "source_adapters_touch_no_helper": true, + "helper_dimension_census": { + "0->4": 26, + "0->8": 6, + "0->9": 326, + "1->8": 6, + "1->9": 41, + "2->9": 1, + "5->9": 2 + }, + "rigid_zero_entrance_helper_count": 358, + "paid_only_nonzero_entrance_helper_count": 50, + "selected_paid_edge_occurrences": 1016, + "paths_edge_occurrence_disjoint": true, + "source_geodesic_rank_census": { + "4": 2, + "7": 7, + "8": 41 + }, + "owned_center_profile_fixed": { + "8": 8 + }, + "baseline_paid_profile": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "baseline_helper_profile": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + } + }, + "backward": { + "program_sha256": "a4ff7b7ca8f23c858f8e6f1044bc6abf92168ab17abd2aa420ad384f58a519d3", + "nodes": 19197, + "paid_edge_occurrences": 34398, + "native_edge_occurrences": 240, + "source_native_ranks_all_zero": true, + "source_main_adapter_occurrences": 448, + "source_adapters_touch_no_helper": true, + "helper_dimension_census": { + "0->4": 26, + "0->8": 6, + "0->9": 326, + "1->8": 6, + "1->9": 41, + "2->9": 1, + "5->9": 2 + }, + "rigid_zero_entrance_helper_count": 358, + "paid_only_nonzero_entrance_helper_count": 50, + "selected_paid_edge_occurrences": 1016, + "paths_edge_occurrence_disjoint": true, + "source_geodesic_rank_census": { + "4": 2, + "7": 7, + "8": 41 + }, + "owned_center_profile_fixed": { + "8": 8 + }, + "baseline_paid_profile": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "baseline_helper_profile": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + } + } + }, + "rank_metric": "d(L,M)=9-dim(L intersect M), L(F)=F^-1(Z)", + "fixed_height": "k(L)=dim(proj_x L)=d(L,Z)", + "path_debt_inequality": "sum(H(r_i+delta_i)-H(r_i)) >= H(sum(r_i)+sum(delta_i))-H(sum(r_i))", + "proof_domain": "H(x)=x^t, H(0)=0, 0>n)).bit_count()+((b&mask)&(a>>n)).bit_count())%2 + layer={()} + for k in range(n): + nxt=set() + for rows in layer: + old=span(rows) + for v in range(1,1<<(2*n)): + if v not in old and all(pairing(v,x)==0 for x in rows):nxt.add(basis((*rows,v))) + layer=nxt + return sorted(layer) + +def calibrate(): + results=[] + for n,count in [(1,3),(2,15),(3,135)]: + charts=all_lagrangians(n);need(len(charts)==count,'complete small Lagrangian count') + mask=(1<=abs(k-l),'arbitrary phase chart projection lower bound') + results.append({'dimension':n,'lagrangians':len(charts),'ordered_pairs':len(charts)**2}) + return results diff --git a/research/productive-helper-dimension-floor/check.py b/research/productive-helper-dimension-floor/check.py new file mode 100644 index 0000000000..44805ea4d9 --- /dev/null +++ b/research/productive-helper-dimension-floor/check.py @@ -0,0 +1,303 @@ +"""Source-bound fixed-projection-height Clifford invoice obstruction. + +For an inverse-image Clifford chart L=F^-1(Z), its x-projection height is +k(L)=d(L,Z), where d(L,M)=9-dim(L intersect M) is the Fourier-rank metric. +Fixing each node's source height makes every paid rank at least its original +nested rank. The 358 zero-entrance helpers have fixed residual rank. Each of +the other 50 helpers has a native-free paid wire path whose source rank sum +equals its residual rank. These paths share no paid edge occurrence. + +If one path has source ranks r_i, increases delta_i>=0, and R=sum(r_i), +concavity of H(x)=x**t (0= H(R+sum(delta_i))-H(R). +The rank triangle inequality bounds the changed helper residual by +R+sum(delta_i), so its entire additional credit is funded by that path. +Source native costs are zero, and owned-center tariffs remain fixed. +Therefore neither frozen orientation has a cheaper complete invoice, even +with arbitrary quadratic Clifford charts of the fixed projection heights. + +This verifies source incidences and the hypotheses of the written proof; +it is not a proof-kernel certificate or a new physical supplier admission. +Only the Python standard library is used. All checks survive python -O. +""" +from pathlib import Path +from collections import Counter +import argparse +import copy +import gzip +import hashlib +import json + + +SOURCE_SHA256 = 'cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd' +EXPECTED_PAID = Counter({1: 2201, 2: 412, 3: 510, 4: 127, 5: 40, 8: 8}) +EXPECTED_HELPERS = Counter({4: 28, 7: 7, 8: 47, 9: 326}) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def span(vectors): + result = {0} + for vector in vectors: + result |= {x ^ vector for x in tuple(result)} + return frozenset(result) + + +def dimension(space): + need(len(space) > 0 and not len(space) & (len(space)-1), 'subspace cardinality') + return len(space).bit_length()-1 + + +def map_vector(columns, vector): + result = 0 + for bit, column in enumerate(columns): + if vector >> bit & 1: + result ^= column + return result + + +def inverse(columns): + values = {map_vector(columns, x): x for x in range(512)} + need(len(values) == 512, 'invertible native map') + return tuple(values[1 << i] for i in range(9)) + + +def canonical_hash(value): + raw = json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + return hashlib.sha256(raw).hexdigest() + + +def source_graph(payload, direction='forward'): + """Reconstruct chronological contacts and every persistent wire incidence.""" + need(direction in ('forward', 'backward'), 'known program orientation') + program = payload['programs'][direction] + canonical = payload['canonical'] + frames = list(map(span, canonical['frames'])) + need(canonical['h'] == 9 and len(canonical['start']) == len(canonical['final']) == 632, + 'source dimensions') + need(all(dimension(s) == len(b) for s, b in zip(frames, canonical['frames'])), + 'independent canonical frame bases') + maps = {w['op']: tuple(w['G_columns']) for w in canonical['warps']} + maps.update({-op: inverse(g) for op, g in list(maps.items())}) + nodes, edges, adapter_roles = [], [], [] + paths = [[] for _ in range(632)] + + def node(label): + index = len(nodes) + nodes.append(label) + return index + + def edge(kind, start, end, role, rank, event): + index = len(edges) + edges.append({'kind': kind, 'a': start, 'b': end, 'role': role, + 'rank': rank, 'event': event}) + paths[role].append(index) + + current = [node(label) for label in canonical['start']] + entrances = current[:] + for event_index, event in enumerate(program): + kind = event[0] + if kind == 'scalar': + gate, label = event[1:] + refs = gate[1:3] if gate[0] in ('add', 'copy') else gate[1:2] + contact = node(label) + for role_kind, role in refs: + if role_kind != 'L': + continue + old = nodes[current[role]] + need(frames[old] <= frames[label], 'every source paid edge nested') + edge('paid', current[role], contact, role, + dimension(frames[label])-dimension(frames[old]), event_index) + current[role] = contact + elif kind == 'warp': + _, role_ref, op, source, target = event + need(role_ref[0] == 'L', 'persistent native occurrence') + role = role_ref[1] + left, right = node(source), node(target) + old = nodes[current[role]] + need(frames[old] <= frames[source], 'source paid pre-warp nesting') + edge('paid', current[role], left, role, + dimension(frames[source])-dimension(frames[old]), event_index) + need(frozenset(map_vector(maps[op], v) for v in frames[source]) == frames[target], + 'source native rank zero') + edge('native', left, right, role, 0, event_index) + current[role] = right + elif kind == 'adapter': + need(len(event) == 4 and event[1] in ('old_to_new', 'new_to_old') + and type(event[2]) is int and 0 <= event[2] < 224, + 'source adapters touch only main roles') + adapter_roles.append(event[2]) + else: + need(kind in ('climb', 'center', 'phase'), 'known source event') + + exits = [] + for role, label in enumerate(canonical['final']): + final = node(label) + exits.append(final) + old = nodes[current[role]] + need(frames[old] <= frames[label], 'source final nesting') + edge('paid', current[role], final, role, + dimension(frames[label])-dimension(frames[old]), len(program)) + + paid = Counter(e['rank'] for e in edges if e['kind'] == 'paid' and e['rank']) + emitted = Counter(e[5] for e in program if e[0] == 'climb') + need(paid == emitted, 'all positive source paid occurrences reconstructed') + centers = Counter(e[4] for e in program if e[0] == 'center') + need(centers == Counter({8: 8}) and paid+centers == EXPECTED_PAID, + 'complete source invoice') + need(Counter(adapter_roles) == Counter({role: 2 for role in range(224)}), + 'both source main adapter boundaries') + + nonzero_entrances, zero_entrances = [], [] + helper_dimensions, helper_ranks = Counter(), Counter() + for role in range(224, 632): + start = frames[canonical['start'][role]] + finish = frames[canonical['final'][role]] + k, l = dimension(start), dimension(finish) + need(start < finish, 'source helper strictly nested and productive') + helper_dimensions[k, l] += 1 + helper_ranks[l-k] += 1 + (nonzero_entrances if k else zero_entrances).append(role) + need(len(nonzero_entrances) == 50 and len(zero_entrances) == 358, + 'complete helper entrance partition') + need(helper_ranks == EXPECTED_HELPERS, 'source helper rank census') + return {'nodes': nodes, 'edges': edges, 'frames': frames, + 'paths': {role: paths[role] for role in nonzero_entrances}, + 'entrances': entrances, 'exits': exits, 'centers': centers, + 'paid': paid, 'helper_dimensions': helper_dimensions, + 'helper_ranks': helper_ranks, 'nonzero_entrances': nonzero_entrances, + 'zero_entrances': zero_entrances, 'adapter_roles': adapter_roles} + + +def check_paths(graph, paths): + """Check every nonzero-entrance helper's complete actual paid wire path.""" + need(sorted(paths) == graph['nonzero_entrances'], + 'every nonzero-entrance helper path covered') + all_ids = [index for ids in paths.values() for index in ids] + need(len(all_ids) == len(set(all_ids)), 'path paid edge occurrences disjoint') + result = [] + for role, ids in paths.items(): + need(ids, 'nonempty helper path') + current = graph['entrances'][role] + ranks, positive = [], [] + for index in ids: + need(type(index) is int and 0 <= index < len(graph['edges']), 'path edge range') + edge = graph['edges'][index] + need(edge['kind'] == 'paid', 'path has no native operation') + need(edge['role'] == role and edge['a'] == current, + 'continuous actual helper-wire path') + current = edge['b'] + ranks.append(edge['rank']) + if edge['rank']: + positive.append({'edge': index, 'event': edge['event'], + 'rank': edge['rank'], 'a': edge['a'], 'b': edge['b']}) + need(current == graph['exits'][role], 'complete helper entry to exit path') + start = graph['frames'][graph['nodes'][graph['entrances'][role]]] + finish = graph['frames'][graph['nodes'][graph['exits'][role]]] + k, l = dimension(start), dimension(finish) + need(0 < k < l <= 9 and start < finish, 'source helper endpoint heights') + need(sum(ranks) == l-k, 'source helper path geodesic') + result.append({'role': role, 'entrance_node': graph['entrances'][role], + 'exit_node': graph['exits'][role], 'entrance_height': k, + 'exit_height': l, 'source_helper_rank': l-k, + 'edge_occurrences': ids, 'positive_source_edges': positive, + 'path_rank_mass': sum(ranks)}) + need(len(all_ids) == 1016, 'complete selected paid path occurrence census') + return result + + +def verify(payload): + need(canonical_hash(payload) == SOURCE_SHA256, 'source payload hash') + directions = {} + for direction in ('forward', 'backward'): + graph = source_graph(payload, direction) + paths = check_paths(graph, graph['paths']) + directions[direction] = { + 'program_sha256': canonical_hash(payload['programs'][direction]), + 'nodes': len(graph['nodes']), + 'paid_edge_occurrences': sum(e['kind'] == 'paid' for e in graph['edges']), + 'native_edge_occurrences': sum(e['kind'] == 'native' for e in graph['edges']), + 'source_native_ranks_all_zero': True, + 'source_main_adapter_occurrences': len(graph['adapter_roles']), + 'source_adapters_touch_no_helper': True, + 'helper_dimension_census': {str(k)+'->'+str(l): v for (k, l), v + in sorted(graph['helper_dimensions'].items())}, + 'zero_entrance_helpers': graph['zero_entrances'], + 'rigid_zero_entrance_helper_count': len(graph['zero_entrances']), + 'paid_only_nonzero_entrance_helper_count': len(paths), + 'selected_paid_edge_occurrences': sum(len(p['edge_occurrences']) for p in paths), + 'paths_edge_occurrence_disjoint': True, + 'source_geodesic_rank_census': dict(sorted(Counter(p['source_helper_rank'] for p in paths).items())), + 'paths': paths, + 'owned_center_profile_fixed': dict(sorted(graph['centers'].items())), + 'baseline_paid_profile': dict(sorted((graph['paid']+graph['centers']).items())), + 'baseline_helper_profile': dict(sorted(graph['helper_ranks'].items()))} + return { + 'status': 'PASS_FIXED_PROJECTION_HEIGHT_CLIFFORD_OBSTRUCTION', + 'source_sha256': SOURCE_SHA256, + 'directions': directions, + 'rank_metric': 'd(L,M)=9-dim(L intersect M), L(F)=F^-1(Z)', + 'fixed_height': 'k(L)=dim(proj_x L)=d(L,Z)', + 'path_debt_inequality': 'sum(H(r_i+delta_i)-H(r_i)) >= H(sum(r_i)+sum(delta_i))-H(sum(r_i))', + 'proof_domain': 'H(x)=x^t, H(0)=0, 0