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.
Two-triangle hybrid RT0 local elimination
Statement
Assume Countable Choice.
Split the unit square by its diagonal into and . For unit permeability and on , on , the hybrid solution has where and . The local elimination equations reduce to , , , and ; changing shifts both pressures by the same constant and is precisely the gauge.
Facts & Assumptions
Given: The two-triangle mesh, unit permeability, and source values on equal-area cells.
Countable Choice is inherited from the hybrid equivalence and local flux suppliers. (The Axiom of Countable Choice ())
The local hybrid equations use the cell energy, pressure-divergence term, facet multiplier, cell balance and matching-flux equations. (Hybridized no-flow RT0/P0 Darcy system)
Cell balances and the constant pressure gauge have the meanings stated in the hybridization theorem. (Hybridization, static condensation, and pressure gauge)
Gauss–Green gives the integral of divergence as total outward facet flux on each triangle. (Gauss–Green formula on an affine simplex)
RT0 facet fluxes are unisolvent; imposing zero flux on two facets leaves a one-dimensional local flux space. (RT0 facet-flux unisolvence and global H(div) conformity)
Proof
Each cell has area . The field has zero normal component on and , and unit integrated outward flux on the diagonal from ; has zero normal component on and , and unit integrated outward flux on the diagonal from . Their divergences are both , so by [F3]. The two zero-boundary conditions and the single free facet degree of freedom make each a basis of its local space by [F4]. Direct integration gives and reflection symmetry gives .
Write . The cell balances in [F1] give and . For a local test , its integrated divergence is and its interior outward flux is . The first hybrid equation is therefore for every real , equivalently . The jump equation is , which the balance values satisfy.
Solving the local equations gives and . Since the cells have equal area, their global mean is ; choose the mean-zero gauge to obtain the stated pressures. After local elimination the single skeleton equation is , independent of , so its one-dimensional nullspace consists exactly of common constant shifts. This is the constant gauge described in [F2].
Mesh diagram
The shared diagonal is the only interior facet. Flux arrows are schematic; the proof computes their exact integrated outward values as and .
Depends on
- Hybridized no-flow RT0/P0 Darcy system
- Hybridization, static condensation, and pressure gauge
- Exact RT0/P0 element mass balance and normal continuity
- Affine simplicial meshes and RT/BDM spaces
- RT0 facet-flux unisolvence and global H(div) conformity
- Gauss–Green formula on an affine simplex
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
33 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Francisco-Javier Sayas, A gentle introduction to the Finite Element Method (2015) (standard reference, not scraped)
- Daniele Boffi, Franco Brezzi and Michel Fortin, Mixed Finite Element Methods and Applications (standard reference, not scraped)