where dimensions run out

import%20marimo%0A%0A__generated_with%20%3D%20%220.23.14%22%0Aapp%20%3D%20marimo.App(width%3D%22medium%22)%0A%0A%0A%40app.cell%0Adef%20_()%3A%0A%20%20%20%20import%20marimo%20as%20mo%0A%0A%20%20%20%20return%20(mo%2C)%0A%0A%0A%40app.cell%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(r%22%22%22%0A%20%20%20%20%23%20Where%20Dimension%20Vectors%20Run%20Out%0A%0A%20%20%20%20Every%20units%20library%20agrees%20that%20%60meter%20%2B%20second%60%20is%20illegal.%20That%20layer%20%E2%80%94%20dimensions%0A%20%20%20%20as%20exponent%20vectors%20%E2%80%94%20is%20a%20solved%20problem.%20The%20interesting%20question%20is%20what%20happens%0A%20%20%20%20when%20dimensions%20**agree**%20but%20the%20quantities%20are%20still%20different%20*sorts*%20of%20thing.%0A%0A%20%20%20%20Astropy%20already%20answered%20this%20once%3A%20it%20refuses%20%60rad%20%E2%86%92%20sr%60%2C%20treating%20angle%20as%20more%0A%20%20%20%20than%20a%20bare%20dimensionless%20number.%20This%20notebook%20takes%20that%20decision%20seriously%20as%0A%20%20%20%20**prior%20art**%2C%20shows%20where%20the%20general%20version%20of%20the%20problem%20still%20bites%0A%20%20%20%20(in%20astropy%2C%20in%20pint%2C%20and%20%E2%80%94%20out%20of%20the%20box%20%E2%80%94%20in%20ucon%20too)%2C%20and%20demonstrates%20one%0A%20%20%20%20general%20mechanism%20for%20closing%20it%3A%20a%20kind%20lattice%20with%20explicit%20join%20policies.%0A%0A%20%20%20%20Everything%20below%20executes%20live.%20Nothing%20is%20mocked.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_()%3A%0A%20%20%20%20import%20astropy.units%20as%20u%0A%20%20%20%20import%20pint%0A%0A%20%20%20%20from%20ucon%20import%20Number%2C%20units%2C%20active_kinds%0A%0A%20%20%20%20ureg%20%3D%20pint.UnitRegistry()%0A%20%20%20%20Q%20%3D%20ureg.Quantity%0A%20%20%20%20lattice%20%3D%20active_kinds()%0A%20%20%20%20return%20Number%2C%20Q%2C%20lattice%2C%20u%2C%20units%0A%0A%0A%40app.cell%0Adef%20_()%3A%0A%20%20%20%20def%20trial(label%2C%20fn)%3A%0A%20%20%20%20%20%20%20%20%22%22%22Run%20fn%3B%20report%20either%20its%20value%20or%20the%20refusal.%22%22%22%0A%20%20%20%20%20%20%20%20try%3A%0A%20%20%20%20%20%20%20%20%20%20%20%20result%20%3D%20fn()%0A%20%20%20%20%20%20%20%20%20%20%20%20return%20f%22%7C%20%60%7Blabel%7D%60%20%7C%20%E2%9C%85%20computes%20%7C%20%60%7Bresult%7D%60%20%7C%22%0A%20%20%20%20%20%20%20%20except%20Exception%20as%20e%3A%0A%20%20%20%20%20%20%20%20%20%20%20%20msg%20%3D%20str(e).replace(%22%7C%22%2C%20%22%5C%5C%7C%22)%0A%20%20%20%20%20%20%20%20%20%20%20%20if%20len(msg)%20%3E%2090%3A%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20msg%20%3D%20msg%5B%3A90%5D%20%2B%20%22%E2%80%A6%22%0A%20%20%20%20%20%20%20%20%20%20%20%20return%20f%22%7C%20%60%7Blabel%7D%60%20%7C%20%F0%9F%9B%91%20refuses%20%7C%20%60%7Btype(e).__name__%7D%3A%20%7Bmsg%7D%60%20%7C%22%0A%0A%20%20%20%20def%20table(title%2C%20rows)%3A%0A%20%20%20%20%20%20%20%20header%20%3D%20f%22**%7Btitle%7D**%5Cn%5Cn%7C%20expression%20%7C%20outcome%20%7C%20detail%20%7C%5Cn%7C---%7C---%7C---%7C%5Cn%22%0A%20%20%20%20%20%20%20%20return%20header%20%2B%20%22%5Cn%22.join(rows)%0A%0A%20%20%20%20return%20table%2C%20trial%0A%0A%0A%40app.cell%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(r%22%22%22%0A%20%20%20%20%23%23%201.%20The%20shared%20foundation%0A%0A%20%20%20%20Dimension-vector%20arithmetic.%20All%20three%20libraries%20refuse%20to%20add%20a%20length%20to%20a%20time.%0A%20%20%20%20No%20disagreement%20here%20%E2%80%94%20this%20is%20the%20floor%2C%20not%20the%20ceiling.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_(Number%2C%20Q%2C%20mo%2C%20table%2C%20trial%2C%20u%2C%20units)%3A%0A%20%20%20%20_rows%20%3D%20%5B%0A%20%20%20%20%20%20%20%20trial(%22astropy%3A%201*u.m%20%2B%201*u.s%22%2C%20lambda%3A%201%20*%20u.m%20%2B%201%20*%20u.s)%2C%0A%20%20%20%20%20%20%20%20trial(%22pint%3A%20%20%20%20Q(1%2C'm')%20%2B%20Q(1%2C's')%22%2C%20lambda%3A%20Q(1%2C%20%22m%22)%20%2B%20Q(1%2C%20%22s%22))%2C%0A%20%20%20%20%20%20%20%20trial(%0A%20%20%20%20%20%20%20%20%20%20%20%20%22ucon%3A%20%20%20%20Number(1%2C%20meter)%20%2B%20Number(1%2C%20second)%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20lambda%3A%20Number(1%2C%20units.meter)%20%2B%20Number(1%2C%20units.second)%2C%0A%20%20%20%20%20%20%20%20)%2C%0A%20%20%20%20%5D%0A%20%20%20%20mo.md(table(%22Length%20%2B%20time%22%2C%20_rows))%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(r%22%22%22%0A%20%20%20%20%23%23%202.%20Astropy's%20prior%20art%3A%20angle%20is%20not%20nothing%0A%0A%20%20%20%20Dimensionally%2C%20an%20angle%20is%20a%20ratio%20of%20lengths%20%E2%80%94%20pure%20number.%20Astropy%20nevertheless%0A%20%20%20%20refuses%20to%20conflate%20radians%20with%20plain%20scalars%2C%20and%20refuses%20%60rad%20%E2%86%92%20sr%60.%0A%20%20%20%20This%20is%20the%20important%20concession%3A%20**dimension%20vectors%20under-determine%20legality**%2C%0A%20%20%20%20and%20astropy's%20designers%20knew%20it.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_(mo%2C%20table%2C%20trial%2C%20u)%3A%0A%20%20%20%20_rows%20%3D%20%5B%0A%20%20%20%20%20%20%20%20trial(%0A%20%20%20%20%20%20%20%20%20%20%20%20%22astropy%3A%201*u.rad%20%2B%201%20(dimensionless)%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20lambda%3A%201%20*%20u.rad%20%2B%201%20*%20u.dimensionless_unscaled%2C%0A%20%20%20%20%20%20%20%20)%2C%0A%20%20%20%20%20%20%20%20trial(%22astropy%3A%20(1*u.rad).to(u.sr)%22%2C%20lambda%3A%20(1%20*%20u.rad).to(u.sr))%2C%0A%20%20%20%20%5D%0A%20%20%20%20mo.md(table(%22Astropy's%20angle%20handling%22%2C%20_rows))%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(r%22%22%22%0A%20%20%20%20%23%23%203.%20The%20same%20probes%20in%20pint%0A%0A%20%20%20%20Pint%20takes%20the%20strict%20dimensional-vector%20view%3A%20radian%20*is*%20dimensionless%2C%0A%20%20%20%20so%20everything%20collapses.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_(Q%2C%20mo%2C%20table%2C%20trial)%3A%0A%20%20%20%20_rows%20%3D%20%5B%0A%20%20%20%20%20%20%20%20trial(%22pint%3A%20Q(1%2C'rad')%20%2B%20Q(1)%22%2C%20lambda%3A%20Q(1%2C%20%22radian%22)%20%2B%20Q(1))%2C%0A%20%20%20%20%20%20%20%20trial(%22pint%3A%20Q(1%2C'rad').to('sr')%22%2C%20lambda%3A%20Q(1%2C%20%22radian%22).to(%22steradian%22))%2C%0A%20%20%20%20%5D%0A%20%20%20%20mo.md(table(%22Pint's%20angle%20handling%22%2C%20_rows))%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(r%22%22%22%0A%20%20%20%20%23%23%204.%20The%20general%20problem%3A%20gray%20vs.%20sievert%0A%0A%20%20%20%20Absorbed%20dose%20(Gy)%20and%20dose%20equivalent%20(Sv)%20are%20both%20J%2Fkg.%20They%20are%20related%20by%20an%0A%20%20%20%20empirical%2C%20tissue-dependent%20quality%20factor%20%E2%80%94%20adding%20or%20converting%20them%20silently%20is%20a%0A%20%20%20%20physically%20meaningless%20operation%20that%20radiation-protection%20practice%20exists%20to%20prevent.%0A%0A%20%20%20%20Astropy%20*labels*%20both%20with%20the%20same%20physical%20type%2C%20but%20the%20label%20does%20not%20gate%0A%20%20%20%20arithmetic.%20Pint%20sees%20only%20L%C2%B2%2FT%C2%B2.%20And%20%E2%80%94%20stated%20plainly%20%E2%80%94%20**bare%20ucon%20%60Number%60%0A%20%20%20%20arithmetic%20does%20the%20same%20thing**%2C%20because%20by%20default%20it%20enforces%20dimensions%20only.%0A%20%20%20%20The%20angle%20special-case%20does%20not%20generalize%20in%20any%20of%20the%20three%20defaults.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_(Number%2C%20Q%2C%20mo%2C%20table%2C%20trial%2C%20u%2C%20units)%3A%0A%20%20%20%20_rows%20%3D%20%5B%0A%20%20%20%20%20%20%20%20trial(%22astropy%3A%201*u.Gy%20%2B%201*u.Sv%22%2C%20lambda%3A%201%20*%20u.Gy%20%2B%201%20*%20u.Sv)%2C%0A%20%20%20%20%20%20%20%20trial(%22astropy%3A%20(1*u.Gy).to(u.Sv)%22%2C%20lambda%3A%20(1%20*%20u.Gy).to(u.Sv))%2C%0A%20%20%20%20%20%20%20%20trial(%22pint%3A%20%20%20%20Q(1%2C'Gy')%20%2B%20Q(1%2C'Sv')%22%2C%20lambda%3A%20Q(1%2C%20%22gray%22)%20%2B%20Q(1%2C%20%22sievert%22))%2C%0A%20%20%20%20%20%20%20%20trial(%0A%20%20%20%20%20%20%20%20%20%20%20%20%22ucon%3A%20%20%20%20Number(1%2C%20gray)%20%2B%20Number(1%2C%20sievert)%20%20%20%23%20default%20mode%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20lambda%3A%20Number(1%2C%20units.gray)%20%2B%20Number(1%2C%20units.sievert)%2C%0A%20%20%20%20%20%20%20%20)%2C%0A%20%20%20%20%5D%0A%20%20%20%20_note%20%3D%20(%0A%20%20%20%20%20%20%20%20%22%5Cn%5CnEvery%20row%20above%20that%20computes%20is%20producing%20a%20number%20with%20no%20physical%20meaning.%20%22%0A%20%20%20%20%20%20%20%20%22The%20astropy%20physical%20type%20for%20both%20units%20is%20%22%0A%20%20%20%20%20%20%20%20f%22%60%7Bu.Gy.physical_type%7D%60%20%E2%80%94%20the%20annotation%20exists%2C%20but%20nothing%20enforces%20it.%22%0A%20%20%20%20)%0A%20%20%20%20mo.md(table(%22Gray%20%2B%20sievert%2C%20three%20defaults%22%2C%20_rows)%20%2B%20_note)%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(r%22%22%22%0A%20%20%20%20%23%23%205.%20Closing%20the%20gap%3A%20kinds%20as%20declared%20epistemics%0A%0A%20%20%20%20ucon's%20answer%20is%20a%20**kind%20lattice**%20layered%20above%20the%20dimension%20vector.%20A%20kind%20states%0A%20%20%20%20what%20*sort*%20of%20quantity%20a%20number%20is%20(%60absorbed_dose%60%2C%20%60dose_equivalent%60%2C%20%60torque%60%2C%0A%20%20%20%20%60energy%60%2C%20%E2%80%A6).%20Kinds%20are%20opt-in%20declarations%20%E2%80%94%20no%20magic%20inference%20%E2%80%94%20and%20the%20lattice%0A%20%20%20%20carries%20**join%20policies**%3A%20when%20two%20kinds%20meet%20under%20%60%2B%60%2C%20the%20operation%20resolves%0A%20%20%20%20their%20least%20common%20ancestor%20and%20consults%20its%20policy.%20%60specific_energy%60%20says%0A%20%20%20%20*refuse*%2C%20so%20Gy%20%2B%20Sv%20dies%20loudly%2C%20with%20the%20policy%20named%20in%20the%20error.%0A%0A%20%20%20%20The%20same%20mechanism%2C%20with%20zero%20special-casing%2C%20separates%20torque%20from%20energy%20%E2%80%94%0A%20%20%20%20astropy%20merges%20these%20into%20a%20single%20physical%20type%20(%60energy%2Ftorque%2Fwork%60).%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_(Number%2C%20lattice%2C%20mo%2C%20table%2C%20trial%2C%20units)%3A%0A%20%20%20%20_k_abs%20%3D%20lattice.get(%22absorbed_dose%22)%0A%20%20%20%20_k_eq%20%3D%20lattice.get(%22dose_equivalent%22)%0A%20%20%20%20_k_torque%20%3D%20lattice.get(%22torque%22)%0A%20%20%20%20_k_energy%20%3D%20lattice.get(%22energy%22)%0A%0A%20%20%20%20_rows%20%3D%20%5B%0A%20%20%20%20%20%20%20%20trial(%0A%20%20%20%20%20%20%20%20%20%20%20%20%22ucon%3A%20Gy%E2%9F%A8absorbed_dose%E2%9F%A9%20%2B%20Sv%E2%9F%A8dose_equivalent%E2%9F%A9%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20lambda%3A%20Number(1%2C%20units.gray%2C%20kind%3D_k_abs)%0A%20%20%20%20%20%20%20%20%20%20%20%20%2B%20Number(1%2C%20units.sievert%2C%20kind%3D_k_eq)%2C%0A%20%20%20%20%20%20%20%20)%2C%0A%20%20%20%20%20%20%20%20trial(%0A%20%20%20%20%20%20%20%20%20%20%20%20%22ucon%3A%20N%C2%B7m%E2%9F%A8torque%E2%9F%A9%20%2B%20J%E2%9F%A8energy%E2%9F%A9%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20lambda%3A%20Number(1%2C%20units.newton%20*%20units.meter%2C%20kind%3D_k_torque)%0A%20%20%20%20%20%20%20%20%20%20%20%20%2B%20Number(1%2C%20units.joule%2C%20kind%3D_k_energy)%2C%0A%20%20%20%20%20%20%20%20)%2C%0A%20%20%20%20%20%20%20%20trial(%0A%20%20%20%20%20%20%20%20%20%20%20%20%22ucon%3A%20rad%20%2B%20sr%20%20%20(no%20kinds%20needed%20%E2%80%94%20genuine%20dimensions)%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20lambda%3A%20Number(1%2C%20units.radian)%20%2B%20Number(1%2C%20units.steradian)%2C%0A%20%20%20%20%20%20%20%20)%2C%0A%20%20%20%20%5D%0A%20%20%20%20mo.md(table(%22Kind-annotated%20arithmetic%22%2C%20_rows))%0A%20%20%20%20return%0A%0A%0A%40app.cell%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(r%22%22%22%0A%20%20%20%20%23%23%206.%20What%20this%20is%20(and%20is%20not)%0A%0A%20%20%20%20Three%20postures%20toward%20the%20same%20underlying%20fact%3A%0A%0A%20%20%20%20-%20**pint**%20%E2%80%94%20the%20dimension%20vector%20is%20the%20whole%20story%3B%20everything%20dimensionless%20collapses.%0A%20%20%20%20-%20**astropy**%20%E2%80%94%20the%20vector%20under-determines%20legality%2C%20patched%20where%20it%20hurt%20most%0A%20%20%20%20%20%20(angles)%2C%20with%20descriptive-but-unenforced%20physical%20types%20elsewhere.%0A%20%20%20%20-%20**ucon**%20%E2%80%94%20the%20patch%20generalized%3A%20pseudo-dimensions%20at%20the%20unit%20layer%20where%0A%20%20%20%20%20%20quantities%20are%20structurally%20distinct%20(angle%2Fsolid%20angle)%2C%20a%20kind%20lattice%20above%20it%0A%20%20%20%20%20%20where%20they%20are%20distinct%20only%20*in%20sort*%20(Gy%2FSv%2C%20torque%2Fenergy)%2C%20and%20explicit%2C%0A%20%20%20%20%20%20machine-readable%20refusals%20(%60JoinRefused%60%2C%20named%20join%20policies)%20when%20legality%0A%20%20%20%20%20%20cannot%20be%20established.%0A%0A%20%20%20%20ucon%20is%20a%20**verifier%2C%20not%20a%20solver**%3A%20it%20confirms%20algebraic%20legality%3B%20it%20does%20not%0A%20%20%20%20supply%20quality%20factors%2C%20resolve%20ambiguity%2C%20or%20guess%20intent.%20The%20Gy%E2%86%92Sv%20relationship%0A%20%20%20%20is%20empirically%20constituted%20by%20measurement%20procedure%20%E2%80%94%20exactly%20the%20kind%20of%20thing%20an%0A%20%20%20%20algebra%20should%20refuse%20to%20invent.%0A%0A%20%20%20%20*Every%20result%20in%20this%20notebook%20was%20produced%20by%20the%20code%20shown%2C%20at%20run%20time.*%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0Aif%20__name__%20%3D%3D%20%22__main__%22%3A%0A%20%20%20%20app.run()%0A