Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A coordinate shear preserves Jordan content by translating every section

Example

Fix iji\ne j and cRc\in\mathbb R. The coordinate shear S(x1,,xn)=(x1,,xj+cxi,,xn)S(x_1,\ldots,x_n)=(x_1,\ldots,x_j+cx_i,\ldots,x_n) preserves the Jordan content of every bounded Jordan set.

Facts & Assumptions

Given: The displayed shear SS and bounded Jordan set EE.

[L1]

For a bounded Jordan set whose sections are Jordan measurable outside a content-zero set of parameters, the completed sectional-content function is integrable and its integral is the content of the set (Cavalieri: Jordan content is the integral of sectional contents, and equal sections give equal content).

Verification

technique · direct
1.1

The shear matrix is the identity with one off-diagonal entry cc, so its determinant is 11. By [L2] the linear image S(E)S(E) is Jordan measurable and cont(S(E))=1cont(E)=cont(E)\operatorname{cont}(S(E))=|1|\operatorname{cont}(E)=\operatorname{cont}(E).

L2given
2.1

Sections show the same thing wherever [L1] applies. Hold all coordinates except xjx_j fixed: the corresponding section of S(E)S(E) is the section of EE translated by cxicx_i, so its one-dimensional content is unchanged, and for a set whose sections are Jordan outside a content-zero parameter set [L1] integrates these equal values to the same total. This is a second reading of the result and not a second proof of it: a bounded Jordan set need not have Jordan sections outside a content-zero parameter set, so [L1] is not available for an arbitrary EE and step 1.1 carries the statement.

L1step 1.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 82 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources